library SPASSTest

spec Bar =

sorts A < B; C < B;

sorts alone[1],lone[$$]

end

spec Bar_Ops =

Bar

then

op a : B * B -> alone[1];

a : B * A -> alone[1];

c1,c2,c3 : alone[1];

__+*__ : B * B -> lone[$$];

b1,b2,b3: B

pred PR: alone[1] * B

forall x,y : B

. a(x,y) = c1 when x in A else (c2 when x in C else c3) %(++)%

then

forall x,y : B

. b1 =

b2 when a(x,y) = (c1 when x in B else c3) else b3

then

forall x,y : B

. b1 when a(x,y) = c1 else b2 = b2 when a(x,y) = c3 else b3

then

forall x,y : B

. PR(a(x,y) when true else a(y,x),

b1 when (true <=> false) else b2)

then %implies

forall x : A; y : B

. a(x,y) = c1 %(G1)%

forall x,y : B

. PR(a(x,y),b2) %(G3)%

. false %(is_inconsistent)%

end

spec Bar_Preds =

Bar

then

preds P1 : A * B;

P1 : alone[1] * A;

__elem__ : A * lone[$$]

end

spec Bar_union =

Bar_Ops and Bar_Preds

end

spec Overload_Test =

Bar_union

then

pred a : A * C

sort a

end

spec EmptySort =

sort s

then %implies

. exists x:s . x in s %(trivial_non_empty_test)%

end

spec FreeTest =

free type X ::= X | X1 | e

then %implies

. not X1 = X %(simple_disjoint)%

spec PredicateLogic =

preds A,B,C : ()

. A => B %(ax1)%

. B <=> C %(ax2)%

then %implies

. A => C %(g1)%

end

spec OverloadTest =

sort A < B; C

free type BC ::= sorts B,C

ops g_in : A -> B;

g_in : B -> BC;

g_in : C -> BC

end

spec PredOverloadTest =

sorts A ,B < C

pred P : A * A;

P : B * B

. exists x : C . not (x as A) in A %(A_is_proper_subset)%

forall x : C

. (x in A) => not (x in B)

spec PredOverloadTest2 =

sorts A,B < C; A,B < D; w < A; x < B

pred P : C * C;

P : D * D

. exists x : C . not (x as A) in A %(A_is_proper_subset)%

forall x : C

. (x in A) => not (x in B)

spec InconsTest =

{} and PredOverloadTest

then %implies

. false %(inconsistent)%

spec Sokrates =

sort Top

pred Mortal : Top;

Human : Top

op sokrates : Top

forall x : Top

. Human(x) => Mortal(x) %(all_humans_are_mortal)%

. Human(sokrates) %(sokrates_is_a_human)%

then %implies

. Mortal(sokrates) %(sokrates_is_mortal)%

. false %(is_inconsistent)%

then %implies

forall x,y:Top

. Mortal(x) => Human(x) %( )%

end

spec Inconsistent =

sorts A,B

free type C ::= sorts A,B

sorts ill < A; ill < B

ops a1 : A;

b1 : B

then %implies

. false %(is_inconsistent)%

. not a1 in ill %(a1_in_ill)%

. not b1 in ill %(b1_in_ill)%

. forall x : C . not x in ill %(x_C_in)%

end

spec GenTest =

sort A,B

generated type Foo ::= sorts A,B | c1

free type List_A ::= cons(A;List_A) | nil

then %implies

forall x : A; l : List_A

. not (cons(x,l) = nil) %(disjoint_constructors)%

. false %(is_inconsistent)%

end

spec GenTest2 =

sorts A,B

free type Foo ::= sorts A,B | c1

free type Maybe[Foo] ::= sort Foo | Nothing

then %implies

forall x : A; y : B

. not x = c1 %(free1)%

. not x in B %(free2)%

. not c1 = Nothing %(free3)%

. not x = Nothing %(free4)%

. not y = Nothing %(free5)%

. x in Maybe[Foo] %(injection1)%

. y in Maybe[Foo] %(injection2)%

end

spec GenTest2a =

GenTest2

then

op a1: A

then %implies

. not a1 in B %(wrong_sort_test)%

. not a1 = c1 %(equal_test5)%

. a1 = c1 %(equal_test5a)%

then %implies

. not (a1 as B) in B %(cast_test1)%

then %implies

. not (a1 : Foo as B) in B %(cast_test2)%

. not (a1 as B) in B %(cast_test3)%

. not def (a1 as B) %(cast_test4)%

end

spec UniqueExt =

sort s

pred UC : s

op c:s

. UC(c) %(c is in UC)%

. exists! x: s . UC(x) %(only one element in UC)%

then %implies

forall x : s

. UC(x) <=> x = c %(everything in UC is equal to c)%

end

spec Keywords =

preds False,True: ()

sort s

op status : s

spec Eq_Pred =

sort s

op f1,f2 : s * s -> s

pred __eq__ : s * s;

EQUAL(x,y:s) <=> x = y %(axiom_should_be_removed_1)%

forall x, y,z:s

. x = y <=> y eq x %(axiom_should_be_removed_2)%

. EQUAL(x,z) => z=x %(axiom_should_be_modified_1)% %implied

. EQUAL(x,y) /\ y eq z => x=z %(axiom_should_be_modified_2)% %implied

. f1(x,y) = x when EQUAL(y,x) /\

y eq (x when exists w:s . w eq y

else f2(y,x))

else y %(no predication should be there)%

. not y eq x if not x = y %(short Th)% %implied

. x eq z if EQUAL(x,y) /\ z = y %(short Th)% %implied

. not x eq y if not y = x /\ x = x %(short Th)% %implied

. x eq z if EQUAL(x,y) /\ z = y /\ z = z %(short Th)% %implied

. z=z %(short Th)% %implied

. x=x %(3)% %implied

. y=y %(three)% %implied

spec small = {}

spec Reserved_Words = sort comp,Foo

then %implies

. false %(inconsistent)%