Algebraic implementations preserve program correctness

DOI10.1016/0167-6423(86)90004-3MaRDI QIDQ1079358zbMATH OpenOpenAlexFDO

Authors Manfred Broy, Bernhard Möller, Peter Pepper, Martin Wirsing

Publication date 1986

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(86)90004-3

zbMATH Keywords

abstract data typesAlgebraic specificationCorrectnessimplementations

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Algebraic specification of data types are a method for giving a precise formal description of the computation structures to be used in a software project. After the validation of an algebraic specification an implementation of these computation structures has to be developed, if the computation structures are to be used. In constrast to approaches where concrete models of data types are constructed it is suggested in this paper to replace an algebraic specification by another one which is closer to the computation structures available in the target machine or the target language. Correctness criteria are given that guarantee the preservation of partial or total correctness of programs when replacing the given algebraic specifications on which the programs operate by the new ones. This way the concept of algebraic implementations and their correctness is obtained. Moreover the transitivity of implementations is shown.

Recommendations

• On algebra of program correctness and incorrectness
• scientific article; zbMATH DE number 3954253
• scientific article; zbMATH DE number 5181785
• Algebras for program correctness in Isabelle/HOL
• scientific article; zbMATH DE number 3872655
• Combining algebraic specifications and procedural tools for correct program development
• Building program construction and verification tools from algebraic principles
• scientific article; zbMATH DE number 6403889
• Recent advances in program verification through computer algebra
• Algebraic translations, correctness and algebraic compiler construction

Cited in

(9)

• Structured algebraic specifications: A kernel language
• Toward formal development of programs from algebraic specifications: Implementations revisited
• Crypt-equivalent algebraic specifications
• Equational specification of partial higher-order algebras
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• A semi-algorithm for algebraic implementation proofs
• Algebraic implementation of abstract data types: a survey of concepts and new compositionality results
• Hybrid implementations of algebraic specifications
• Implementation of data types by algebraic methods

This page was built for publication: Algebraic implementations preserve program correctness

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