3.1 CASL Equational Specifications

Roughly speaking, the considered CASL equational specifications consist of many-sorted conditional equational axioms. The equality predicate is used to express the congruence on terms, whereas the equivalence predicate is used for the congruence on boolean expressions.

3.1.1 Basic CASL specifications

Definition. Let Sigma be a many-sorted first-order signature, such that Sigma_S, Sigma_F, Sigma_P denote respectively the set of sorts, the set of ranked function symbols, and the set of ranked predicate symbols. Let X be a set of sorted variables, where sorts are taken from Sigma_S. The set of many-sorted terms built over the signature Sigma and the set of variables X is denoted T(Sigma_F,X). The set of CASL boolean expressions CBE(Sigma,X) is the set smallest set such that:

• false e CBE(Sigma,X) and true e CBE(Sigma,X)
• If p: s₁ ×...×s_n e Sigma_P, and t₁:s₁,..., t_n:s_n are terms in T(Sigma_F,X), then p(t₁,...,t_n) e CBE(Sigma,X)
• If t₁:s,t₂:s e T(Sigma_F,X), then t₁=t₂ e CBE(Sigma,X)
• If b e CBE(Sigma,X), then (not  b) e CBE(Sigma,X)
• If b₁,b₂ e CBE(Sigma,X), then b₁ /\ b₂ e CBE(Sigma,X), b₁ \/ b₂ e CBE(Sigma,X), and b₁ <=> b₂ e CBE(Sigma,X)

The set of CASL equational formulas CF(Sigma,X) is the smallest set such that:

• If f: s₁ ×...×s_n -> s e Sigma_F, and t₁:s₁,..., t_n:s_n, t:s, and b e CBE(Sigma,X), then (f(t_1,...,t_n) = t  if  b) e CF(Sigma,X)
• If p: s₁ ×...×s_n e Sigma_P, and t₁:s₁,..., t_n:s_n are terms in T(Sigma_F,X), and b,b' e CBE(Sigma,X), then (p(t_1,...,t_n) <=> b'  if  b) e CF(Sigma,X)

A CASL equational specification is given by a tuple (Sigma, V, CF) where V is a finite subset of X and CF is a finite subset of CF(Sigma,V).

In the current implementation, the following abbreviations are available.

• f(t₁,...,t_n) = t, instead of (f(t₁,...,t_n) = t  if  true)
• p(t₁,...,t_n) <=> b', instead of (p(t₁,...,t_n) <=> b'  if  true)
• (p(t₁,...,t_n)  if  b), instead of (p(t₁,...,t_n) <=> true  if  b)
• (not  p(t₁,...,t_n)  if  b), instead of (p(t₁,...,t_n) <=> false  if  b)

Using the CASL concrete syntax, a CASL equational specification has to be defined as follows.

Example. (CASL equational specification skeleton).

spec
     Module = 
     sort
         {s}(s  $e$  SigmaS) 
     ops
         {f}(f  $e$  SigmaF) 
     preds
         {p}(p  $e$  SigmaP) 
     vars
         {v}(v  $e$  V) 
     { . phi}(phi  $e$  CF) 

3.1.2 Structured CASL specifications

It is important to note that we are able to deal with CASL specifications which are not simply defined as in Example 3.1.1, but these complicated specifications can be reduced to basic (flat) ones thanks to the CASL tool set:

• Structured CASL specifications. The CASL tool set [Mos00][MKKB97] transforms a structured specification into a flat one, by using the so-called FCasEnv output parse tree (see Section 4.1).
• Mixfix operators. The CASL tool set is able to parse mixfix operators.

Example. Consider the following basic CASL specification:

spec 
     INTEG =
     sort 
         Integ 
     ops
         plus: Integ * Integ -> Integ;
         s: Integ -> Integ;
         zero : Integ;

     vars
         x : Integ ;
         y : Integ

     . plus(zero,y) = y
     . plus(s(x),y) = s(plus(x,y))

This basic specification can be imported in the structured specification below:

from INTEG get INTEG

spec 
     GT_pred = 
     INTEG then

     preds
         __ > __ : Integ * Integ 

     vars
         x : Integ ;
         y : Integ
    
     . s(x) > s(y) <=> x > y
     . s(x) > zero
     . not (zero > s(x))
     . not (zero > zero)

The latter is equivalent to the basic (flat) CASL specification:

spec 
     GT_pred_basic = 
     sort 
         Integ 
     ops
         plus: Integ * Integ -> Integ;
         s: Integ -> Integ;
         zero : Integ;
     preds
         __ > __ : Integ * Integ 

     vars
         x : Integ ;
         y : Integ
    
     . plus(zero,y) = y
     . plus(s(x),y) = s(plus(x,y))

     . s(x) > s(y) <=> x > y
     . s(x) > zero
     . not (zero > s(x))
     . not (zero > zero)