Toward formal development of programs from algebraic specifications: Implementations revisited

DOI10.1007/BF02737104MaRDI QIDQ1090100zbMATH OpenOpenAlexFDO

Authors Donald Sannella, Andrzej Tarlecki

Publication date 1988

Published in Acta Informatica (Search for Journal in Brave)

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

zbMATH Keywords

abstractor implementationsconstructor implementationsinstitutionprogram development processrefinement

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Publication:4721633
• scientific article; zbMATH DE number 3954253
• Combining algebraic specifications and procedural tools for correct program development
• scientific article; zbMATH DE number 3936498
• scientific article; zbMATH DE number 4043230

Cites work

• A Deductive Approach to Program Synthesis
• A theory of type polymorphism in programming
• Algebraic and operational semantics of specifications allowing exceptions and errors
• Algebraic implementation of abstract data types
• Algebraic implementations preserve program correctness
• Axioms for abstract model theory
• Final Data Types and Their Specification
• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3864486 (Why is no real title available?)
• scientific article; zbMATH DE number 3876564 (Why is no real title available?)
• scientific article; zbMATH DE number 3880083 (Why is no real title available?)
• scientific article; zbMATH DE number 3819086 (Why is no real title available?)
• scientific article; zbMATH DE number 3821084 (Why is no real title available?)
• scientific article; zbMATH DE number 3821094 (Why is no real title available?)
• scientific article; zbMATH DE number 3823106 (Why is no real title available?)
• scientific article; zbMATH DE number 3898210 (Why is no real title available?)
• scientific article; zbMATH DE number 3898213 (Why is no real title available?)
• scientific article; zbMATH DE number 3898214 (Why is no real title available?)
• scientific article; zbMATH DE number 3909717 (Why is no real title available?)
• scientific article; zbMATH DE number 3911679 (Why is no real title available?)
• scientific article; zbMATH DE number 3911689 (Why is no real title available?)
• scientific article; zbMATH DE number 3918620 (Why is no real title available?)
• scientific article; zbMATH DE number 3936493 (Why is no real title available?)
• scientific article; zbMATH DE number 3938540 (Why is no real title available?)
• scientific article; zbMATH DE number 3949706 (Why is no real title available?)
• scientific article; zbMATH DE number 3963900 (Why is no real title available?)
• scientific article; zbMATH DE number 3714904 (Why is no real title available?)
• scientific article; zbMATH DE number 3714981 (Why is no real title available?)
• scientific article; zbMATH DE number 3729432 (Why is no real title available?)
• scientific article; zbMATH DE number 3754008 (Why is no real title available?)
• scientific article; zbMATH DE number 3765116 (Why is no real title available?)
• scientific article; zbMATH DE number 3774870 (Why is no real title available?)
• scientific article; zbMATH DE number 3776831 (Why is no real title available?)
• scientific article; zbMATH DE number 3529404 (Why is no real title available?)
• scientific article; zbMATH DE number 3582349 (Why is no real title available?)
• scientific article; zbMATH DE number 3640837 (Why is no real title available?)
• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• scientific article; zbMATH DE number 3995031 (Why is no real title available?)
• scientific article; zbMATH DE number 3997131 (Why is no real title available?)
• scientific article; zbMATH DE number 3999262 (Why is no real title available?)
• Initial Algebra Semantics and Continuous Algebras
• LCF considered as a programming language
• On observational equivalence and algebraic specification
• On the existence of free models in abstract algebraic institutions
• On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types
• Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
• Partial abstract types
• Programming in a wide spectrum language: A collection of examples
• Quasi-varieties in abstract algebraic institutions
• Report on the Larch shared language
• Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
• Specifications, models, and implementations of data abstractions
• Structured algebraic specifications: A kernel language
• Testing equivalences for processes

Cited in

(45)

• HasCasl: integrated higher-order specification and program development
• Constructing specification morphisms
• Toward formal development of programs from algebraic specifications: Parameterisation revisited
• Two impossibility theorems on behaviour specification of abstract data types
• Structured theory presentations and logic representations
• Behavioural approaches to algebraic specifications. A comparative study
• Essential concepts of algebraic specification and program development
• Proof systems for structured specifications with observability operators
• The definition of Extended ML: A gentle introduction
• Swinging types=functions+relations+transition systems
• A hidden agenda
• Observational proofs by rewriting.
• A logic for the stepwise development of reactive systems
• Modular specification of process algebras
• Prelogical relations
• Observational interpretations of hybrid dynamic logic with binders and silent transitions
• Hybrid dynamic logic institutions for event/data-based systems
• Abstract implementation of algebraic specifications in a temporal logic language
• Views on behaviour protocols and their semantic foundation
• Lambda expressions in Casl architectural specifications
• Algebraic signatures enriched by dependency structure
• Dynamic logic with binders and its application to the development of reactive systems
• Heterogeneous Logical Environments for Distributed Specifications
• A coalgebraic perspective on logical interpretations
• scientific article; zbMATH DE number 3921971 (Why is no real title available?)
• scientific article; zbMATH DE number 3936498 (Why is no real title available?)
• scientific article; zbMATH DE number 3954253 (Why is no real title available?)
• scientific article; zbMATH DE number 1121419 (Why is no real title available?)
• scientific article; zbMATH DE number 1368953 (Why is no real title available?)
• scientific article; zbMATH DE number 3995031 (Why is no real title available?)
• Definition-like Extensions by Sorts
• A theory of requirements capture and its applications
• Proving correctness w.r.t. specifications with hidden parts
• Proving the correctness of behavioural implementations
• Toward formal development of programs from algebraic specifications: model-theoretic foundations
• The foundational legacy of ASL
• Observational interpretation of Casl specifications
• scientific article; zbMATH DE number 5499339 (Why is no real title available?)
• ZB 2005: Formal Specification and Development in Z and B
• Combining algebraic specifications and procedural tools for correct program development
• Behavioural theories and the proof of behavioural properties
• On behavioural abstraction and behavioural satisfaction in higher-order logic
• On the correctness of modular systems
• Generic constructions for behavioral specifications
• A language for configuring multi-level specifications

Describes a project that uses

Uses Software

• ML

This page was built for publication: Toward formal development of programs from algebraic specifications: Implementations revisited

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