Toward formal development of programs from algebraic specifications: Implementations revisited

DOI10.1007/BF02737104zbMath0621.68004OpenAlexW4249644839MaRDI QIDQ1090100

Andrzej Tarlecki, Donald Sannella

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

refinementinstitutionabstractor implementationsconstructor implementationsprogram development process

Mathematics Subject Classification ID

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

Related Items (34)

Structured theory presentations and logic representations ⋮ A language for configuring multi-level specifications ⋮ Views on Behaviour Protocols and Their Semantic Foundation ⋮ Lambda Expressions in Casl Architectural Specifications ⋮ Algebraic Signatures Enriched by Dependency Structure ⋮ A theory of requirements capture and its applications ⋮ Behavioural approaches to algebraic specifications. A comparative study ⋮ 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 ⋮ Essential concepts of algebraic specification and program development ⋮ Proving correctness w.r.t. specifications with hidden parts ⋮ Proving the correctness of behavioural implementations ⋮ Proof systems for structured specifications with observability operators ⋮ The definition of Extended ML: A gentle introduction ⋮ Observational interpretations of hybrid dynamic logic with binders and silent transitions ⋮ Behavioural theories and the proof of behavioural properties ⋮ On behavioural abstraction and behavioural satisfaction in higher-order logic ⋮ On the correctness of modular systems ⋮ A logic for the stepwise development of reactive systems ⋮ Toward formal development of programs from algebraic specifications: Model-theoretic foundations ⋮ Observational interpretation of Casl specifications ⋮ HasCasl: integrated higher-order specification and program development ⋮ Modular specification of process algebras ⋮ Hybrid dynamic logic institutions for event/data-based systems ⋮ Generic constructions for behavioral specifications ⋮ Swinging types=functions+relations+transition systems ⋮ A hidden agenda ⋮ The Foundational Legacy of ASL ⋮ Prelogical relations ⋮ Observational proofs by rewriting. ⋮ Constructing specification morphisms ⋮ Toward formal development of programs from algebraic specifications: Parameterisation revisited ⋮ Two impossibility theorems on behaviour specification of abstract data types

Uses Software

• ML

Cites Work

• Algebraic and operational semantics of specifications allowing exceptions and errors
• Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
• Report on the Larch shared language
• Algebraic implementations preserve program correctness
• Structured algebraic specifications: A kernel language
• On the existence of free models in abstract algebraic institutions
• On observational equivalence and algebraic specification
• Quasi-varieties in abstract algebraic institutions
• Programming in a wide spectrum language: A collection of examples
• Specifications, models, and implementations of data abstractions
• Algebraic implementation of abstract data types
• Partial abstract types
• LCF considered as a programming language
• A theory of type polymorphism in programming
• Testing equivalences for processes
• A Deductive Approach to Program Synthesis
• On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types
• Final Data Types and Their Specification
• Axioms for abstract model theory
• Initial Algebra Semantics and Continuous Algebras
• Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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