3.3 Translation from CASL to ELAN

The translation is defined by using a straightforward mapping between CASL boolean expressions and ELAN ones, and a mapping between CASL formulas and ELAN ones. Moreover CASL predicates are viewed as ELAN functions with bool (an ELAN built-in sort) as codomains.

Definition. Given a many-sorted first-order signature Sigma, Sigma' denotes the many-sorted first-order signature defined as follows:

• Sigma_S' = Sigma_S
• Sigma_F' = Sigma_F U { p: s₁ ×...×s_n -> bool }_{p : s1 ×...×sn} e Sigma_P
• Sigma_P'=Ø

The mapping tr_B: CBE(Sigma,X) -> EBE(Sigma',X) is defined recursively as follows:

• tr_B(false) := false
• tr_B(true) := true
• tr_B(p(t₁,...,t_n)) := p(t₁,...,t_n)
• tr_B(t₁=t₂) := t₁ = t₂
• tr_B(not  b) := not  b
• tr_B(b₁ /\ b₂) : = b₁  and  b₂
• tr_B(b₁ \/ b₂) : = b₁  or  b₂
• tr_B(b₁ <=> b₂) : = b₁ = b₂

The mapping tr_F: CF(Sigma,X) -> EF(Sigma',X) is defined as follows:

• tr_F(f(t₁,...,t_n) = t  if  b) := f(t₁,...,t_n) -> t  if  tr_B(b)
• tr_F(p(t₁,...,t_n) <=> b'  if  b) := p(t₁,...,t_n) -> tr_B(b')  if  tr_B(b)

The ELAN translation of a CASL equational specification (Sigma,V,CF) is the ELAN equational specification (Sigma',V,tr_F(CF)).

From now on, the ELAN translation of a CASL equational specification is assumed to be confluent and terminating.

Example. (Example 3.1.2 continued) This ELAN translation of the CASL equational basic specification GT_pred_basic is as follows.

module GT_pred_basic

sort Integ ;
end

operators global

         plus(@,@): (Integ Integ) Integ ;
         s(@): (Integ) Integ ;
         zero: Integ ;
         @ > @ : (Integ Integ) bool ; 
end

rules for bool
   x : Integ ;
   y : Integ
global    
 [] plus(zero,y) => y end
 [] plus(s(x),y) => s(plus(x,y)) end
 [] s(x) > s(y)  => x > y end
 [] s(x) > zero  => true end
 [] zero > s(x)  => false end
 [] zero > zero  => false end
end

end // of module