Name
Abstract | ||
|---|---|---|
Practical specification languages for imperative and object-oriented programs, such as JML, Eiffel, and Spec#, allow the use of program expressions including method calls in specification formulas. For coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be weakly pure in the sense that their evaluation has no effect on the state of preexisting objects. For specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. Calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. This paper formalizes a notion of observational purity, justifies the use of weakly and observationally pure methods in specifications, and shows that a method is observationally pure if it simulates a weakly pure method. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.tcs.2007.02.004 | Theor. Comput. Sci. |
Keywords | Field | DocType |
specification formula,mutate state,method call,large system,standard method,weakly pure method,information hiding,practical specification language,standard library,benevolent side effects,coherent semantics,specification and verification,observationally pure method,observational purity,object oriented programming | Specification language,Programming language,Object-oriented programming,Computer science,Assertion,Imperative programming,Theoretical computer science,Implementation,Lazy initialization,Spec#,Eiffel | Journal |
Volume | Issue | ISSN |
376 | 3 | Theoretical Computer Science |
Citations | PageRank | References |
10 | 0.58 | 23 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| David Naumann | 1 | 1101 | 84.12 |