Modular Specification and Verification of Functional Behavior
In the following three chapters, we present our modular specification and verification technique for Mojave programs, beginning with the so-called functional behavior of methods. Under functional behavior, we subsume the deliberate effects of a method: the computation of a result value and modifications to the object store. That is, “functional” does not mean “side-effect-free”. We describe our specification technique for functional behavior based on abstract fields and pre-post-pairs, illustrate modular verification of functional behavior, and discuss related work.
KeywordsProgramming Logic Open Program Information Hiding Functional Behavior Proof Obligation
Unable to display preview. Download preview PDF.