Go backward to Subsorts and Overloading
Go up to CASL
Go forward to Sort Generation Constraints
Formulae
The usual first-order quantification and logical connectives
are provided.
Many algebraic specification frameworks allow quantifiers and the
usual logical connectives: the adjective `algebraic' refers to the
specification of algebras, not to a possible restriction to purely
equational specifications, which are algebraic in a different sense.
But of course many prototyping systems do restrict specifications to
(conditional) equations, so as to be able to use term rewriting
techniques in tools; this will be reflected in restrictions of CASL to
sublanguages.
Predicates for use in atomic formulae may be declared.
It is quite common practice to eschew the use of predicates, taking
(total) functions with results in some built-in sort of truth-values
instead. As with restrictions to conditional equations, this may be
convenient for prototyping, but it seems difficult to motivate at the
level of using CASL for general specification and verification.
Hence predicates may be declared, and combined using the standard
logical connectives.
CoFI Tentative Document: Mosses97TAPSOFT --TAPSOFT'97-- April 1997.
Comments to pdmosses@brics.dk