Name
Abstract | ||
|---|---|---|
Anecdotal experience constructing proofs of correctness of code built from reusable software components reveals that they tend to be relatively trivial bookkeeping exercises: they rarely require a substantive mathematical deduction. A careful empirical analysis of hundreds of verification conditions (VCs) for a library of component-client code shows the level of sophistication each proof requires, and suggests how to use the results to characterize a notion of mathematical "obviousness." |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04211-9_4 | ICSR |
Keywords | Field | DocType |
deep mathematics,trivial bookkeeping,reusable software component,careful empirical analysis,anecdotal experience,simple bookkeeping,verifying component-based software,verification condition,substantive mathematical deduction,component-client code,software component | Programming language,Computer science,Correctness,Reusable software,Mathematical proof,Loop invariant,Software,Bookkeeping,Software construction,Sophistication | Conference |
Volume | ISSN | Citations |
5791 | 0302-9743 | 7 |
PageRank | References | Authors |
0.55 | 9 | 7 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jason Kirschenbaum | 1 | 68 | 5.59 |
| Bruce Adcock | 2 | 70 | 4.79 |
| Derek Bronish | 3 | 93 | 6.47 |
| Hampton Smith | 4 | 56 | 5.01 |
| Heather Harton | 5 | 56 | 4.00 |
| Murali Sitaraman | 6 | 270 | 40.99 |
| Bruce W. Weide | 7 | 575 | 182.57 |