Modular Specification and Verification of Frame Properties
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.
KeywordsAbstract Location Regular Expression Proof Obligation Method Invocation Dynamic Dependency
Unable to display preview. Download preview PDF.