Modular correctness proofs of behavioural implementations

DOI10.1007/S002360050149MaRDI QIDQ1127821zbMATH OpenOpenAlexFDO

Authors Rolf Hennicker, Michel Bidoit

Publication date 29 March 1999

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s002360050149

zbMATH Keywords

algebraic specificationsbehavioural equality

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Review text

We introduce a concept of behavioural implementation for algebraic specifications which is based on an indistinguishability relation (called behavioural equality). Our central objective is the investigation of proof rules which allow us to establish the correctness of behavioural implementations in a modular (and stepwise) way and, moreover, are practicable enough to induce proof obligations that can be discharged with existing theorem provers. Under certain conditions our proof technique can also be applied for proving the correctness of implementations based on an abstraction equivalence between algebras in the sense of Sannella and Tarlecki. The whole approach is presented in the framework of total algebras and first-order logic with equality.

Recommendations

• Proving the correctness of behavioural implementations
• Modular Verification of Recursive Programs
• On the correctness of modular systems
• Modular verification of higher-order functional programs
• Modular verification of programs with effects and effects handlers
• Correctness proofs for abstract implementations
• Formal reasoning about modules, reuse and their correctness

Cited in

(12)

• A semi-algorithm for algebraic implementation proofs
• scientific article; zbMATH DE number 1696758 (Why is no real title available?)
• Towards behavioral Maude: behavioral membership equational logic
• scientific article; zbMATH DE number 3921953 (Why is no real title available?)
• scientific article; zbMATH DE number 17803 (Why is no real title available?)
• Proving the correctness of behavioural implementations
• Observational interpretation of Casl specifications
• Proving Behavioral Refinements of COL-specifications
• On behavioural abstraction and behavioural satisfaction in higher-order logic
• On the correctness of modular systems
• Behavioral abstraction is hiding information
• Observational implementation of algebraic specifications

Describes a project that uses

Uses Software

• LARCH

This page was built for publication: Modular correctness proofs of behavioural implementations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1127821)