4 Comparison

Researchers have only recently begun to study the problems and possible solutions described above. As mentioned in the introduction, related work focuses on the development, specification, and verification of basic components. We summarize this work in the following.

Specification Techniques The two-tiered approach to specifications was introduced by the Larch project (cf. [GH93]). We took this framework as a basis of our work. As described in section 3.1.1, we use a different technique to specify invariance properties which is more appropriate for verification. For the same reason, we use explicit abstraction functions to relate object structures and abstract values. Larch uses implicit abstraction. The formal semantics of specifications used in this paper was presented in [PH97b]. A similar semantics is used in the Larch/C++ language (cf. [Lea96]), based on our work.

Verification Techniques The verification technique assumed in this paper goes back to [Hoa69]. Programming logics for object-oriented languages can be found in [AL97,PH97b]. [AL97] focuses on the soundness of a logic for an object-based language, whereas [PH97b] concentrates on the relation between specification and verification of object-oriented programs. [Lei95] deals with the construction of verified modular programs. As he does not use the rigor formal semantics of invariants, he does not face many of the problems discussed in this paper.

Language Features Since the notion of behavioral subtyping was introduced in [Ame87], much work has been done in this area. [DL96] discusses the relation of behavioral subtyping and specification inheritance. In particular, this approach is interesting in the context of code inheritance (see section 3.2). The separation of subtyping and code inheritance is realized in the Sather language (cf. [Omo94]). The presented technique has no formal semantics and is, thus, not suitable for verification. Sather supports genericity on a syntactical level by enforcing actual type parameters to be syntactic subtypes of the formal parameter type and inspired thus the technique sketched in section 3.2. Module concepts of existing programming languages work on a syntactical basis only. None of them supports semantic modules or semantical privacy.