Prev Up Next
Go backward to Topdown analysis
Go up to The Vocabulary system
Go forward to The global system specification

Specification on lists, pairs and strings

  1. The list specification:

    The specification of a LIST type which can be take an element as parameter is of fundamental importance as not only the vocabulary system but also strings are instantiations of datatype.

    loose pspec LIST(sort el)
    import el;

    sorts freely generated list;

    constr []: -> list;
    constr add: el x list -> list;
    _._: list x list -> list;
    length: list -> nat;
    _ in _ : el x list -> bool;
    reduceList: list -> list;
    l, m : list
    e1, e2 : el
    [].l = l;
    l.[] = l;
    add(e1, l).m = add(e1, l.m);

    length([]) = 0;
    length(add(e1, l)) = succ(length(l));

    e1 in [] = false;
    e1 in add(e2, l) = (e1 == e2) or e1 in l;

    reduceList([]) = [];
    reduceList(add(e1, l)) =
         if e1 in l then reduceList(l)
        else add(e1, reduceList(l));

    end spec

  2. The PAIR specification:

    All vocabulary entries are pairs, a specification of the datatype can be found below .

    loose pspec PAIR(sort el1, el2)
    import el1;
    import el2;
    sorts freely generated pair;
    constr [_,_]: el1 x el2 -> pair;
    first: pair -> el1;
    second: pair -> el2;
    a: el1;
    b: el2;
    first([a, b]) = a;
    second([a, b]) = b;
    end spec

  3. The STRING specification:

    Strings are list of characters. It can be achieved by renaming (1).

    loose pspec STRING(sort char)
    import char;
    import (LIST(char) rename sort list opns [] to sort string, opn "");
    end spec

Hong Gu (,
Christian Mittermaier (,
Igor Rents (
February 10, 1999

Prev Up Next