Toward formal development of programs from algebraic specifications: Parameterisation revisited
type: Item
instance of: scholarly article
title: Toward formal development of programs from algebraic specifications: Parameterisation revisited
zbMATH Open document ID: 0790.68077
DOI: 10.1007/BF01191893
author: Donald Sannella
author: Stefan Sokołowski
author: Andrzej Tarlecki
published in: Acta Informatica
publication date: 1994-07-04T00:00:00Z
review text: Parameterization is an important mechanism for structuring programs and specifications into modular units. The interplay between parameterization (of programs and of specifications) and specification (of parameterized and of non-parameterized programs) is analyzed, exposing important semantic and methodological differences between specifications of parameterized programs and parameterized specifications. The extension of parameterization mechanisms to the higher-order case is considered, both for parameterized programs and parameterized specifications, and the methodological consequences of such an extension are explored. A specification formalism with parameterization of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satisfies a specification. The formalism includes the basic specification-building operations of the ASL specification language and is institution independent.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 567318
zbMATH Keywords: algebraic specifications
zbMATH Keywords: formal program development
zbMATH Keywords: parameterization
zbMATH Keywords: ASL specification language
describes a project that uses: Nuprl
describes a project that uses: OBSCURE
MaRDI profile type: Publication
cites work: Q3906394
cites work: Q5789040
cites work: Q3660892
cites work: The calculus of constructions
cites work: On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types
cites work: Q3221381
cites work: Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
cites work: Q3197342
cites work: Parameterized Programming
cites work: Q3332238
cites work: A framework for defining logics
cites work: Q3204056
cites work: Q3999860
cites work: Q3677153
cites work: On observational equivalence and algebraic specification
cites work: Specifications in an arbitrary institution
cites work: Toward formal development of programs from algebraic specifications: Implementations revisited
cites work: Q3666260
cites work: Q3723679
cites work: Structured algebraic specifications: A kernel language
Recommended article: Q4721633
Recommended article: Toward formal development of programs from algebraic specifications: Implementations revisited
Recommended article: Toward formal development of programs from algebraic specifications: Model-theoretic foundations
Recommended article: Q4712650
Recommended article: Q2723910
Recommended article: A Calculus of Higher-Order Parameterization for Algebraic Specifications
Recommended article: Combining algebraic specifications and procedural tools for correct program development
Recommended article: An Informal Approach to Formal (Algebraic) Specifications
Recommended article: Q4364371
Recommended article: Foundations of algebraic specification and formal software development.
description: scientific article; zbMATH DE number 567318