Reasoning about data abstraction in contract languages
Ãdám Péter Darvas · Repository for Publications and Research Data (ETH Zurich) · 2009
Due to the large and ever increasing complexity of software systems, abstraction plays an important role in the process of software development.Abstraction is also essential in the formal specification of programs because it allows one to write specifications in an implementation-independent way, which is indispensable for information hiding and facilitates readability and maintainability of specifications.State-of-the-art specification languages provide powerful means of abstraction that are natural to use for programmers.However, previous work provided only partial solutions for reasoning about specifications that make use of these means.This thesis presents techniques that allow one to reason about two means of abstraction that are commonly used in object-oriented specification languages: pure methods and model classes.Pure methods are side-effect free methods of a program.As such, specification languages allow them to be called in specification expressions.In order to reason about calls to pure methods, the methods have to be encoded and axiomatized in the underlying logic of the verification environment.The encoding is non-trivial if pure methods are considered to be weakly-pure, that is, if they are not completely side-effect free and are allowed to allocate, initialize, and return new objects.Such state changes are observable in specification expressions, thus an encoding has to take them into account.The axiomatization of pure methods has to be done with care because unsatisfiable, contradicting, or ill-founded specifications can lead to an inconsistent axiom system if specifications are blindly turned into axioms.This thesis proposes a practical encoding of weakly-pure methods as well as an axiomatization technique that poses proof obligations on specifications that guarantee the consistency of the axiom system that is extracted from the specifications.Model classes are classes that are used only for specification purposes and provide object-oriented interfaces for essential mathematical concepts, such as sets or relations.Specifications can be written in an abstract way by expressing properties in terms of model classes and their operations.A promising approach to reason about specifications that make use of model classes is to map the classes and their operations to the built-in structures and functions of the underlying theorem prover of the verification environi