Advertisement

Modular Specification and Verification of Functional Behavior

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

Abstract

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.

Keywords

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Personalised recommendations