Abstractions of data types

    Authors

    F. L. Tiplea;C. Enea

    Comments

    Authors: contact us about adding a copy of your work at STARS@ucf.edu

    Abbreviated Journal Title

    Acta Inform.

    Keywords

    data type; universal algebra; verification; abstraction; SHAPE-ANALYSIS; Computer Science, Information Systems

    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, for all for all, for all there exists, and there exists(0,1)for all, 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.

    Journal Title

    Acta Informatica

    Volume

    42

    Issue/Number

    8-9

    Publication Date

    1-1-2006

    Document Type

    Article

    Language

    English

    First Page

    639

    Last Page

    671

    WOS Identifier

    WOS:000236641300006

    ISSN

    0001-5903

    Share

    COinS