fmod SYNTAX is pr QID . sorts Var Num Op Exp BVar Boolean BOp BExp Com GuardCom Prog . op V : Qid -> Var . subsort Var < Exp . subsort Num < Exp . op z : -> Num . op s : Num -> Num . ops + - * : -> Op . op ___ : Exp Op Exp -> Exp [prec 20] . op BV : Qid -> BVar . subsort BVar < BExp . subsort Boolean < BExp . ops T F : -> Boolean . ops And Or : -> BOp . op ___ : BExp BOp BExp -> BExp [prec 20] . op Not_ : BExp -> BExp [prec 15] . op Equal : Exp Exp -> BExp . op skip : -> Com . op _:=_ : Var Exp -> Com [prec 30] . op _;_ : Com Com -> Com [assoc prec 40] . op if_fi : GuardCom -> Com [prec 50] . op do_od : GuardCom -> Com [prec 60] . op _->_ : BExp Com -> GuardCom [prec 42] . op _[]_ : GuardCom GuardCom -> GuardCom [assoc prec 45] . subsort Com < Prog . endfm fmod AP is pr SYNTAX . op Ap : Op Num Num -> Num . op _+._ : Num Num -> Num . op _*._ : Num Num -> Num . op _-._ : Num Num -> Num . vars n n' : Num . eq Ap(+,n,n') = n +. n' . eq Ap(*,n,n') = n *. n' . eq Ap(-,n,n') = n -. n' . eq z +. n = n . eq s(n) +. n' = s(n +. n') . eq z *. n = z . eq s(n') *. n = (n' *. n) +. n . eq z -. n = z . eq s(n') -. z = s(n') . eq s(n') -. s(n) = n' -. n . op Ap : BOp Boolean Boolean -> Boolean . op _and_ : Boolean Boolean -> Boolean . op _or_ : Boolean Boolean -> Boolean . var bv bv' : Boolean . eq Ap(And,bv,bv') = bv and bv' . eq Ap(Or,bv,bv') = bv and bv' . eq T and bv = bv . eq F and bv = F . eq T or bv = T . eq F or bv = bv . endfm fmod ENV is inc SYNTAX . sorts Value Variable . subsorts Num Boolean < Value . subsorts Var BVar < Variable . sort ENV . op mt : -> ENV . op _=_ : Variable Value -> ENV [prec 20] . op __ : ENV ENV -> ENV [assoc id: mt prec 30] . op _`(_`) : ENV Var -> Num . op _`(_`) : ENV BVar -> Boolean . op _`[_/_`] : ENV Value Variable -> ENV [prec 35] . op remove : ENV Variable -> ENV . vars X X' : Variable . var V : Value . var ro : ENV . var n : Num . var x : Var . eq remove(mt, X) = mt . eq remove(X = V ro, X') = if X == X' then ro else X = V remove(ro,X') fi . eq ro [V / X] = remove(ro,X) X = V . eq (X = V ro)(X') = if X == X' then V else ro(X') fi . endfm mod COMPUTATION is pr ENV . pr AP . sort Statement . subsorts Num Boolean < Statement . op <_,_> : Exp ENV -> Statement . op <_,_> : BExp ENV -> Statement . op <_,_> : Com ENV -> Statement . op <_,_> : GuardCom ENV -> Statement . sort Statement2 . op `(_,_`) : Com ENV -> Statement2 . op Tick : -> Statement2 . op `(_,_`) : GuardCom ENV -> Statement2 . op fails : -> Statement2 . var n : Num . var x : Var . vars st st' st'' : ENV . vars e e' : Exp . var op : Op . vars v v' : Num . var bx : BVar . var bv bv' : Boolean . var bop : BOp . var be be' : BExp . vars C C' C'' : Com . vars GC GC' : GuardCom . *** Evaluation semantics for expressions, page 94 rl [CR] : < n, st > => n . rl [VarR] : < x, st > => _`(_`)(st,x) . *** if I use mixfix syntax, there are multiple distinct parses ??? crl [OpR] : < e op e', st > => Ap(op,v,v') if < e, st > => v /\ < e', st > => v' . rl [CR] : < T, st > => T . rl [CR] : < F, st > => F . rl [VarR] : < bx, st > => _`(_`)(st,bx) . *** if I use mixfix syntax, there are multiple distinct parses ??? crl [OpR] : < be bop be', st > => Ap(bop,bv,bv') if < be, st > => bv /\ < be', st > => bv' . crl [EqR] : < Equal(e,e'), st > => T if < e, st > => v /\ < e', st > => v . crl [EqR] : < Equal(e,e'), st > => F if < e, st > => v /\ < e', st > => v' /\ v =/= v' . crl [Not] : < Not be, st > => F if < be, st > => T . crl [Not] : < Not be, st > => T if < be, st > => F . *** Computation semantics for GuardL, page 131 crl [AsRc] : < x := e, st > => < skip, st[v / x] > if < e, st > => v . crl [ifRc] : < if GC fi, st > => < C, st > if < GC, st > => < C, st > . crl [ComRc1] : < C ; C', st > => < C'' ; C', st' > if < C, st > => < C'', st' > /\ C =/= C'' . crl [ComRc2] : < C ; C', st > => < C'', st' > if ( C, st ) => Tick /\ < C', st > => < C'', st' > /\ C' =/= C'' . crl [doRc1] : < do GC od, st > => < C ; (do GC od), st > if < GC, st > => < C, st > . crl [doRc2] : < do GC od, st > => < skip, st > if ( GC, st ) => fails . crl [GCRc1] : < be -> C, st > => < C, st > if < be, st > => T . crl [GCRc2] : < GC [] GC', st > => < C, st > if < GC, st > => < C, st > . crl [GCRc2] : < GC [] GC', st > => < C, st > if < GC', st > => < C, st > . *** Failure predicate for GuardL, page 131 crl [IfRf1] : ( be -> C, st ) => fails if < be, st > => F . crl [IfRf2] : ( GC [] GC', st ) => fails if ( GC, st ) => fails /\ ( GC', st ) => fails . *** Termination predicate for GuardL, page 133 rl [Skipt] : ( skip, st ) => Tick . crl [ComRt] : ( C ; C', st ) => Tick if ( C, st ) => Tick /\ ( C', st ) => Tick . endm eof search < if (Equal(V('x), z) -> V('x) := s(z)) [] (Equal(V('x), z) -> V('x) := s(s(z))) fi, V('x) = z > =>+ < skip, ST:ENV > .