Go backward to 2 SORT-ITEM : Some Examples for
DATATYPE-DECL
Go up to Top
Go forward to 4 Some points for discussion
3 SORT-GEN-ITEM : Some Examples
The SORT-GEN-ITEM construct allows to equip sorts and/or
operations with the generation constraint.
This construct is to be used when one wants to express
that the intended models should not allow other ways to obtain data
of the sort corresponding domain (or carrier set) than those specified.
Let us also note that the generation constraint yields an induction
scheme that is useful for theorem proving.
For instance, the following NAT_G specification forbids
a model where the set of integers (with negative numbers) would be a
carrier set for the sort Nat, and provides an induction scheme for Nat
with zero and suc__.
- spec
- NAT_G =
- generated sort
-
- Nat ::= zero | suc__:Nat
-
end
It is also possible to specify that a freely generated constraint as
in NAT_FG below.
Let us note that the use of the freely generated constraint should be
limited to cases where monomorphic data types are intended
(i.e. "true" naturals, "true" lists, etc.).
- spec
- NAT_FG =
- freely generated sort
-
- Nat ::= zero | suc__:Nat
-
end
In practice, it is often a good idea to provide "characteristic" predicates
that can be used to find out how data of a given sort are
generated3.
This is why in the following specification both is_empty and is_unit
are provided.
- spec
- LIST[sort Elem] =
- generated sort
-
- List[Elem] ::=
-
empty |
sort Elem |
__ __:Elem ×List[Elem]
- op
- __is_empty:pred(List[Elem]);
__is_unit:pred(List[Elem])
- axioms
-
empty is_empty;
¬ (e is_empty);
¬ (e l is_empty);
¬ (empty is_unit);
e is_unit;
e l is_unit <=> l is_empty;
e = e empty %% OK since e:List[Elem]
- vars
- e:Elem; l:List[Elem]
- end
-
CoFI
Note: M-2 ---- 5 January 1998.
Comments to Christine.Choppy@irin.univ-nantes.fr