Title

Abstractions Of Data Types

Keywords

Abstraction; Data type; Universal algebra; Verification

Abstract

The use of abstraction in the context of abstract data types, is investigated. Properties to be checked are formulas in a first order logic under Kleene's 3-valued interpretation. Abstractions are defined as pairs consisting of a congruence and a predicate interpretation. Three types of abstractions are considered,∀∀ and ∀∃, and ∃0,1, and for each of them corresponding property preservation results are established. An abstraction refinement property is also obtained. It shows how one can pass from an existing abstraction to a (less) finer one. Finally, equationally specified abstractions in the context of equationally specified abstract data types are discussed and exemplified.

Publication Date

4-1-2006

Publication Title

Acta Informatica

Volume

42

Issue

8-9

Number of Pages

639-671

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.1007/s00236-006-0010-3

Socpus ID

33645674415 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/33645674415

This document is currently not available here.

Share

COinS