Algebraic implementations preserve program correctness
type: Item
instance of: scholarly article
title: Algebraic implementations preserve program correctness
zbMATH Open document ID: 0597.68021
DOI: 10.1016/0167-6423(86)90004-3
author: Manfred Broy
author: Bernhard Möller
author: Peter Pepper
author: Martin Wirsing
published in: Science of Computer Programming
publication date: 1986-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68P05
zbMATH DE Number: 3963177
zbMATH Keywords: abstract data types
zbMATH Keywords: Algebraic specification
zbMATH Keywords: Correctness
zbMATH Keywords: implementations
MaRDI profile type: Publication
full work available at URL: 0167-6423(86)90004-3
OpenAlex ID: W2007398626
Recommended article: On algebra of program correctness and incorrectness
Recommended article: Q3723680
Recommended article: Q5754533
Recommended article: Algebras for Program Correctness in Isabelle/HOL
Recommended article: Q3339261
Recommended article: Combining algebraic specifications and procedural tools for correct program development
Recommended article: Building program construction and verification tools from algebraic principles
Recommended article: Q5173658
Recommended article: Recent advances in program verification through computer algebra
Recommended article: Algebraic translations, correctness and algebraic compiler construction
description: scientific article; zbMATH DE number 3963177