Go backward to Formulae
Go up to CASL
Go forward to Structured Specifications
Sort Generation Constraints
It may be specified that a sort is generated by a set of
functions, so that proof by induction is sound for that sort.
For generality, CASL does not restrict all models to be
finitely-generated (i.e., reachable). The specifier may indicate that
a particular sort (or set of sorts) is to be generated by a particular
set of functions, much as in LARCH.
CoFI Tentative Document: Mosses97TAPSOFT --TAPSOFT'97-- April 1997.
Comments to pdmosses@brics.dk