spec test_if =

pred p,q : ()

. p if q

end

spec test_overloading =

sorts s < t1; t1 < u; s < t2; t2 < u

sorts v < w; w < x

ops f:s->v; f:s->x; f:t1->w %% in the overloading relation

ops g:s->v; g:s->x; g:t1->w %% in the overloading relation

forall y:s

. f(y)=g(y) %(f=g)%

end

spec test_non_overloading =

sorts s < t1; t1 < u; s < t2; t2 < u

sorts v < w; w < x

sorts z1,z2

ops f:s->v; f:s->z1; f:z1->w; f:z2->w %% not in the overloading relation

ops g:s->v; g:s->z1; g:z1->w; g:z2->w %% not in the overloading relation

forall y:s

. (op f : s -> v)(y) = (op g : s -> v)(y) %(f=g 1)%

. (op f : s -> z1)(y) = (op g : s -> z1)(y) %(f=g 2)%

forall y:z1

. f(y) = g(y) %(f=g 3)%

end

spec test_non_overloading2 =

sorts s < t1; t1 < u; s < t2; t2 < u

sorts v < w; w < x

sorts z1,z2

ops f:s->v; f:t1->z1; f:v->w; f:w->t1 %% not in the overloading relation

ops g:s->v; g:t1->z1; g:v->w; g:w->t1 %% not in the overloading relation

end

spec test_partially_overloading =

sorts s < t1; t1 < u; s < t2; t2 < u

sorts v < w; w < x

sort z

ops f:s->v; f:s->x; f:s->z %% partially in the overloading relation

end

spec test_many_sorts =

sorts a,b,c,d,e

end

spec test_connected_components =

sorts a < b; c < b; c < d; d < e; f < e; g < h

end

spec test_cond =

sort s

ops f,g,h:s->s

preds p,q:s

forall x:s

. f(x) = (g(x) when p(x) else h(x))

. f(x) = ((g(x) when p(x) else h(x)) when q(x) else f(x))

end

spec Nat =

free type Nat ::= 0 | suc(Nat)

ops __ + __, __ * __ : Nat * Nat -> Nat;

op ack : Nat * Nat * Nat -> Nat

forall m,n,k : Nat

. 0 + m = m %(add_0_Nat)% %simp

. suc(n) + m = suc(n + m) %(add_suc_Nat)% %simp

. 0 * m = 0 %(mult_0_Nat)% %simp

. suc(n) * m = (n * m) + m %(mult_suc_Nat)% %simp

. m + 0 = m %(add_0_Nat_right)% %implied

%simp

. m+(n+k) = (m+n)+k %(add_assoc_Nat)% %implied

%simp

. m+suc(n) = suc(m+n) %(add_suc_Nat)% %implied

%simp

. m+n = n+m %(add_comm_Nat)% %implied

forall a,b,n:Nat

. ack(a, b, 0)=suc(b)

. ack(a, 0, suc(0))= a

. ack(a, 0, suc(suc(0)))= 0

. ack(a, 0, suc(suc(suc(n))))= suc(0)

. ack(a, suc(b), suc(n))=ack(a, ack(a, b, suc(n)), n)

pred __<=__ : Nat*Nat

forall m,n : Nat

. 0 <= n %(leq_def1_Nat)% %simp

. not suc(n) <= 0 %(leq_def2_Nat)% %simp

. suc(m) <= suc(n) <=> m <= n %(leq_def3_Nat)% %simp

end