Structured Specifications: Syntax, Semantics and Proof Calculus

In this paper, a small but expressive language is presented that allows to write algebraic specifications in a structured and modular way. Proof rules are developed for each construct of the language; in particular, proof systems are given for flat specifications, for structured specifications and the verification of implementations. The language consists of four constructs: one for constructing a flat specification (from a signature and a set of axioms) and three operators for exporting a subsignature, for renaming and for combining specifications.The proof system for flat specifications extends the proof rules of first-order logic by an infinitary rule for relativized quantification w.r.t. standard interpretations of term generated models. Two different techniques for proving the validity of a formula in modular specifications are studied: The first one consists in constructing an equivalent normal form of a structured specification and using a proof system for normal forms, whereas in the second one proofs follow the syntactic structure of the specifications. Finally, a system for proving that a specification is a refinement of another specification is establishedAll proof systems are shown to be sound and relatively complete.