Modular Specification and Verification of Frame Properties

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


In the last chapter, we explained how the functional behavior of methods can be specified and verified. Specification of functional method behavior describes the result value and modifications of the object store, but not the absence of modifications. However, precise information about what is left unchanged by a method execution is crucial for verification. We illustrate that by a small example. Consider the following method that takes a list and a mutable string (we call it StringBuffer as in Java), modifies the string, and appends it to the list. We assume that List and StringBuffer are implemented in different modules that do not import each other.


Abstract Location Regular Expression Proof Obligation Method Invocation Dynamic Dependency 
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