Modular Specification and Verification of Functional Behavior

Part of the Lecture Notes in Computer Science book series (LNCS, volume 2262)


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.


Programming Logic Open Program Information Hiding Functional Behavior Proof Obligation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Personalised recommendations