Go backward to 3 SORT-GEN-ITEM : Some Examples
Go up to Top
Go forward to References
4 Some points for discussion
When selectors are provided as well (hd and tl
in LIST_SEL), although they are included in the generation
constraint, they should not be considered as generators.
- spec
- LIST_SEL[sort Elem] =
- generated sort
-
- List[Elem] ::=
-
empty |
sort Elem |
__ __:(hd:?Elem)×(tl:?List[Elem])
%% hd and tl are partial as indicated by the ?.
- ...
-
- end
-
Let us note that, sometimes, it may be tempting to use the free construct
instead of the generation contraint. However, one should be aware that
(i) these constructs do not yield the same models, (ii) the free construct
provides no induction proof schema, (iii) when using the free construct
one get a generated model in some cases (Horn clauses, flat) but not all ...
In the following specification BASICS, there are four separate
sort generation constraints, and the last sort PhysicalUnit may depend
on the first one PumpNumber.
However, it is ok to have separate generation constraints here since
we have a linearizable hierarchy between these sorts.
- spec
- BASICS =
- generated sort
- PumpNumber ::=
Pump1 | Pump2 |
Pump3 | Pump4;
- generated sort
- PumpState ::= Open | Closed;
- generated sort
- PumpControllerState ::= Flow | NoFlow;
- generated sort
- PhysicalUnit ::=
Pump: PumpNumber
| PumpController: PumpNumber
| OutputStream | WaterLevel;
...
end
Let us now study more closely the following NAT_WEIRD and
NAT_B specifications where there is a mutual dependency
of the sorts Pos and Nat.
- spec
- NAT_WEIRD =
- generated sort
- Zero ::= zero
- generated sort
- Nat ::= Zero | Pos
- generated sort
- Pos ::= succ__:Nat
end
- spec
- NAT_B =
- generated
-
- {
-
- sorts
- Zero ::= zero;
Nat ::= Zero | Pos;
Pos ::= succ__:Nat }
end
NAT_WEIRD and NAT_B are quite different, and this is
due to the fact that the generation constraints are not used in the same
way.
Only NAT_B ensures that both carrier sets are generated (and
do not bear any "junk" value). The fact that the generation constraints
are put separately on the three sorts in NAT_WEIRD entails that
there may be a "junk" value in the Pos carrier set to start with
(i.e. when first used to yield values for the Nat carrier set and
before the generation constraint may be applied), this "junk" value
is then passed on to the Nat carrier set, etc.
What can be noted in this example is that the use of "mutual" subsorts
yields an intertwined situation.
The consequence is that the generation constraints should not be separate
in cases where the use of linear visibility would have been a problem.
CoFI
Note: M-2 ---- 5 January 1998.
Comments to Christine.Choppy@irin.univ-nantes.fr