\documentclass{article}

\usepackage{lstcasl}

\begin{document}

\begin{lstlisting}

library Datatypes

spec Nat =

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

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

forall m,n,k : Nat

. 0 + m = m %(add_0_Nat)%

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

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

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

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

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

end

spec List[sort Elem] =

free type List[Elem] ::= [] | __::__(Elem; List[Elem])

end

spec Partial_Order =

sort Elem

pred __<=__ : Elem * Elem

forall x, y, z:Elem

. x <= x %(reflexive)%

. x <= y /\ y <= x => x=y %(antisymmetric)%

. x <= y /\ y <= z => x <= z %(transitive)%

%{ Note that there may exist x, y such that

neither x <= y nor y <= x. }%

end

spec Total_Order =

Partial_Order

then

forall x, y:Elem

. (x <= y) \/ (y <= x) %(total)%

end

spec ProblematicDefinitionOfSelectors [Total_Order] =

List[sort Elem]

then

ops head : List[Elem] -> Elem;

tail : List[Elem] -> List[Elem];

pred isOrdered : List[Elem]

forall x:Elem; l:List[Elem]

. head(x::l) = x

. tail(x::l) = l

. isOrdered([])

. isOrdered(x::[])

. isOrdered(l) <=> (head(l)<=head(tail(l)) /\ isOrdered(tail(l)))

then %implies

. false

end

spec Char =

free type Char ::= A | B

end

spec String =

List[Char fit Elem |-> Char] with List[Char] |-> String

end

spec StringList =

List[String fit Elem |-> String]

end

spec UnboundedBranchingTree [sort Elem] =

free types

Tree ::= Leaf(Elem) | Branch(Forest);

Forest ::= Nil | Cons(Tree;Forest)

end

\end{lstlisting}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: