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.

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.

scholarly journals Adding Alternative Access Paths to Abstract Data Types

2002 ◽  
pp. 256-267 ◽  
Author(s):  
Xavier Franch ◽  
Jordi Marco
Keyword(s):  
Information Hiding ◽  
Data Type ◽  
Modular Structure ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Programming Framework ◽  
Algebraic Specifications ◽  
Abstract Data ◽  
Adequate Representation

We present in this paper a proposal for developing efficient programs in the abstract data type (ADT) programming framework, keeping the modular structure of programs and without violating the information hiding principle. The proposal focuses in the concept of “shortcut” as an efficient way of accessing to data, alternative to the access by means of the primitive operations of the ADT. We develop our approach in a particular ADT, a store of items. We define shortcuts in a formal manner, using algebraic specifications interpreted with initial semantics, and so the result has a well-defined meaning and fits in the ADT framework. Efficiency is assured with an adequate representation of the type, which provides O(1) access to items in the store without penalising the primitive operations of the ADT.

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>

Sign in / Sign up

Export Citation Format

Share Document