%% ---------------------------------------------------------------------------- %% %% adt.casl %% Abstract Data Types in CASL. %% %% (c) 2016, Wolfgang Schreiner: Thinking Programs. %% %% ---------------------------------------------------------------------------- library adt from Basic/Numbers get Nat %% an initial specification of the type "integer numbers": int(m,n) = m-n spec MyIntCore = Nat then %mono %% hets can't prove that extension by a free spec with axioms is monomorphic %% only that it is conservative free { type Int ::= int(p:Nat;m:Nat) forall n1,n2:Nat . int(suc(n1),suc(n2)) = int(n1,n2) } end %% the type "integer numbers" with auxiliary operations spec MyInt = MyIntCore then %def %% hets can't prove that extension of a free spec with axioms is definitional %% only that it is conservative op 0: Int = int(0,0) op __+__(i1,i2:Int): Int = int(p(i1)+p(i2),m(i1)+m(i2)) pred __<=__(i1,i2:Int) <=> p(i1)+m(i2) <= p(i2)+m(i1) %% alternative definitions of + and <= %{ op __+__: Int * Int -> Int pred __<=__: Int * Int forall p1, m1, p2, m2: Nat . int(p1,m1) + int(p2,m2) = int(p1+p2,m1+m2) . int(p1,m1) <= int(p2,m2) <=> p1+m2 <= p2+m1 }% end %% an initial specification of the type "list of elements" spec ListCore[sort Elem] = %mono %% head and tail are further not used %% by removing their declarations fewer axioms are generated %% which allows hets to quickly prove the %implies extension below %% free type List[Elem] ::= empty | cons(head:?Elem,tail:?List[Elem]) free type List[Elem] ::= empty | cons(Elem,List[Elem]) end %% the type "list of elements" extended by auxiliary operations spec List[sort Elem] given Nat = ListCore[sort Elem] then %def %% alternative definitions of head and tail %{ op head: List[Elem] ->? Elem op tail: List[Elem] ->? List[Elem] forall l:List[Elem]; e:Elem . def head(l) <=> not l = empty . head(cons(e,l)) = e . def tail(l) <=> not l = empty . tail(cons(e,l)) = l }% op append: List[Elem] * List[Elem] -> List[Elem] forall l1,l2:List[Elem]; e:Elem . append(empty,l2) = l2 . append(cons(e,l1),l2) = cons(e,append(l1,l2)) op length: List[Elem] -> Nat forall l:List[Elem]; e:Elem . length(empty) = 0 . length(cons(e,l)) = 1+length(l) end %% the type "list of integers" spec IntList = List[MyInt fit Elem |-> Int] %% generates a proof obligation that can be proved by hets %% using the eprover and the CASL2SoftFOLInduction2 translation spec ListProof[sort Elem] = List[sort Elem] then %implies forall l1,l2:List[Elem] . length(append(l1,l2)) = length(l1)+length(l2) end %% ---------------------------------------------------------------------------- %% end of file %% ----------------------------------------------------------------------------