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;

   opns:

   constr []: -> list;
   constr add: el x list -> list;
   _._: list x list -> list;
   length: list -> nat;
   _ in _ : el x list -> bool;
   reduceList: list -> list;

   vars:

   l, m : list
   e1, e2 : el

   axioms:

   [].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;

   opns:

   constr [_,_]: el1 x el2 -> pair;
   first: pair -> el1;
   second: pair -> el2;

   vars:

   a: el1;
   b: el2;

   axioms:

   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