scholarly journals Unified Algebras and Institutions

1989 ◽  
Vol 18 (274) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Forgetful Functor ◽  
Algebraic Specification ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
Bounded Data ◽  
Data Constraints

<p>A novel framework for algebraic specification of abstract data types is introduced. It involves so-called ''unified algebras'', where sorts are treated as values, so that operations may be applied to sorts as well as to the elements that they classify.</p><p>An institution for unified algebras is defined, and shown to be liberal. However, the ordinary ''forgetful'' functor does not forget any values in unified algebras, so the usual data constraints do not have any models. A ''more forgetful'' functor is introduced and used to define so-called ''bounded'' data constraints, which have the expected models.</p>

The algebraic specification of abstract data types

1978 ◽  
Vol 10 (1) ◽  
Author(s):  
J.V. Guttag ◽  
J.J. Horning
Keyword(s):  
Algebraic Specification ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data

Abstract Data Types, Algebraic Specification

2003 ◽  
pp. 189-201
Author(s):  
Jean-François Monin ◽  
Michael G. Hinchey
Keyword(s):  
Algebraic Specification ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data

scholarly journals Combining Algebraic and Set-Theoretic Specifications (Extended Version)

1996 ◽  
Vol 3 (52) ◽  
Author(s):  
Claus Hintermeier ◽  
Hélene Kirchner ◽  
Peter D. Mosses
Keyword(s):  
Proof Theory ◽  
Type Structure ◽  
Algebraic Specification ◽  
Extended Version ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Horn Clauses ◽  
Algebraic Specifications ◽  
Abstract Data

Specification frameworks such as B and Z provide power sets and cartesian<br />products as built-in type constructors, and employ a rich notation for<br />defining (among other things) abstract data types using formulae of predicate<br />logic and lambda-notation. In contrast, the so-called algebraic specification <br />frameworks often limit the type structure to sort constants and<br />first-order functionalities, and restrict formulae to (conditional) equations.<br />Here, we propose an intermediate framework where algebraic specifications<br />are enriched with a set-theoretic type structure, but formulae remain in the<br />logic of equational Horn clauses. This combines an expressive yet modest<br />specification notation with simple semantics and tractable proof theory.

scholarly journals Unified Algebras and Modules

1988 ◽  
Vol 17 (266) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Specification Language ◽  
Algebraic Specification ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data

This paper concerns the algebraic specification of abstract data types. It introduces and motivates the recently-developed framework of unified algebras, and provides a practical notation for their modular specification. It also compares unified algebras with the well known framework of order-sorted algebras, with underlies of <strong>OBJ</strong> specification language.

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

Sign in / Sign up

Export Citation Format

Share Document