Toward formal development of programs from algebraic specifications: Implementations revisited

DOI10.1007/BF02737104zbMATH Open0621.68004OpenAlexW4249644839MaRDI QIDQ1090100FDOQ1090100

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

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

zbMATH Keywords

refinementinstitutionabstractor implementationsconstructor implementationsprogram development process

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (42)

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

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)