Proof systems for structured specifications and their refinements
The paper constitutes a chapter in a book reporting on the state-of-the-art in the field of algebraic specification and is devoted to proofs of properties of specifications. More precisely, the paper concentrates on proof methodologies for two kinds of properties: the property that a structured specification (i.e. a non-trivial specification built up with the help of operators of a specification language) satisfies a given formula, and the property that a given specification is an implementation of another one (i.e. that the class of models defined by the former specification is a subclass of the class defined by the latter one). To this end the authors successively examine three cases of increasing complexity: structured specifications built up with ``elementary operators, structured specifications with parameters and structured specifications containing reachability and/or observability operators. In each of these three cases the authors distinguish between three proof methodologies: proof systems based on the generation of associated proof rules, proof systems based on the transformation of a specification into a normal form, and ``universal (i.e. Hoare-like) proof systems. The paper is well-structured and clearly written. It has the great merit to present a unified view of the approaches presented by various authors during the last two decades. Due to the technicality of its contents and the use of category theory the paper requires from the reader an appropriate theoretical background. For the entire collection see [Zbl 0973.68002].
- On the lattice of specifications: Applications to a specification methodology
- Proof systems for structured specifications with observability operators
- On normal forms for structured specifications with generating constraints
- CASL: the Common Algebraic Specification Language.
- Logical systems for structured specifications.
- Observational logic, constructor-based logic, and their duality.
- Inductive theorem proving for design specifications
- Strong extension-free proof systems
- Constructor-based observational logic
- Simpler reasoning about system properties: a proof-by-refinement technique
- Compositional modelling and reasoning in an institution for processes and data
- Completeness of a logical system for structured specifications
- scientific article; zbMATH DE number 785047 (Why is no real title available?)
- Proof normalization of structured algebraic specifications is convergent
- Proofs in parameterized specifications
- Proof systems for structured algebraic specifications: An overview
- Property-oriented semantics of structured specifications
- A proof system for conditional algebraic specifications
This page was built for publication: Proof systems for structured specifications and their refinements
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4702601)
