Go backward to 3.6 Attributions
Go up to 3 Basic Specifications
Go forward to 3.8 Datatype Declarations
3.7 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). It is left to the specifier to
express sort generation constraints where appropriate. The CASL
construct for sort generation applies to a group of declarations: the
sorts declared there are constrained to be generated by the
accompanying functions. Thus there is no need to list the sort and
function symbols involved in a sort generation constraint separately
from their declarations, in general.
CoFI
Document: CASL/Rationale --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk