1 Background

Based on a general background in programming language semantics (cf. [PH97a]) and its relation to programming logics, we investigated the formal meaning of interface specifications. This investigation focused on specification techniques for object-oriented programs (cf. [PH95]), because such languages support constructs for component-based programming. In particular, we developed formal foundations for class invariants such that (a) complex linked object structures can be handled and that (b) the invariants can be proved in a Hoare-style logic. Many available object-oriented class libraries work with side-effects; e.g., they support destructive updates on lists. We developed techniques beyond modifies-clauses to express such effects in interface specifications ([MPH97]). In [PH97b], we integrated these ideas within a formal framework for an object-oriented language with recursive classes and recursive methods and provided central verification techniques.