*** the data types for the programming language *** obj ZZ is pr INT . op _is_ : Int Int -> Bool . var I J K L : Int . eq I is I = true . eq (I + J) is (K + J) = I is K . eq (I - J) is (K - J) = I is K . cq I is J = false if (I < J) or (J < I) . eq I + - I = 0 . eq -(I + J) = - I + - J . eq 0 * I = 0 . eq - I * J = -(I * J) . eq I - J = I + - J . eq I * (J + K) = (I * J) + (I * K) . cq I * J = I + (I * (J - 1)) if 0 < J . eq (I + J) * K = (I * K) + (J * K) . eq not(I <= J) = J < I . eq not(I < J) = J <= I . eq I + 1 <= J = I < J . eq I < J + 1 = I <= J . eq I <= J + -1 = I < J . eq I <= J + - K = I + K <= J . eq I < J + - K = I + K < J . eq I + -1 < J = I <= J . eq I <= I = true . eq I < I = false . cq I < I + J = true if 0 < J . eq I + -1 < I = true . cq I + J < I = true if J < 0 . cq I <= J = true if I < J . cq I <= J + 1 = true if I <= J . cq I <= J + K = true if (I <= J) and (I <= K) . cq I + J <= K + L = true if (I <= K) and (J <= L) . endo obj ARRAY is pr ZZ . sort Array . op _[_] : Array Int -> Int [prec 5] . op _[_<-_] : Array Int Int -> Array . var A : Array . var I J K : Int . eq (A [ I <- J ])[I] = J . cq (A [ I <- J ])[K] = A[K] if not(I is K) . endo *** the programming language: expressions *** obj EXP is pr ZZ . dfn Var is QID . sorts Exp Arvar Arcomp . subsorts Var Int Arcomp < Exp . ops a b c : -> Arvar . op _+_ : Exp Exp -> Exp [prec 10] . op _*_ : Exp Exp -> Exp [prec 8] . op -_ : Exp -> Exp [prec 1] . op _-_ : Exp Exp -> Exp [prec 10] . op _[_] : Arvar Exp -> Arcomp [prec 1] . endo *** the programming language: tests *** obj TST is pr EXP . sort Tst . subsort Bool < Tst . op _<_ : Exp Exp -> Tst [prec 15] . op _<=_ : Exp Exp -> Tst [prec 15] . op _is_ : Exp Exp -> Tst [prec 15] . op not_ : Tst -> Tst [prec 1] . op _and_ : Tst Tst -> Tst [prec 20] . op _or_ : Tst Tst -> Tst [prec 25] . endo *** the programming language: basic programs *** obj BPGM is pr TST . sort BPgm . op _:=_ : Var Exp -> BPgm [prec 20] . op _:=_ : Arcomp Exp -> BPgm [prec 20] . endo *** semantics of basic programs *** th STORE is pr BPGM . pr ARRAY . sort Store . op initial : -> Store . op _[[_]] : Store Exp -> Int [prec 65] . op _[[_]] : Store Tst -> Bool [prec 65] . op _[[_]] : Store Arvar -> Array [prec 65] . op _;_ : Store BPgm -> Store [prec 60] . var S : Store . vars X1 X2 : Var . var I : Int . vars E1 E2 : Exp . vars T1 T2 : Tst . var B : Bool . vars AV AV' : Arvar . eq initial [[X1]] = 0 . eq S [[I]] = I . eq S [[- E1]] = -(S[[E1]]) . eq S [[E1 - E2]] = (S[[E1]]) - (S[[E2]]) . eq S [[E1 + E2]] = (S[[E1]]) + (S[[E2]]) . eq S [[E1 * E2]] = (S[[E1]]) * (S[[E2]]) . eq S [[ AV[E1] ]] = (S[[AV]])[ S[[E1]] ] . eq S [[B]] = B . eq S [[E1 is E2]] = (S [[E1]]) is (S [[E2]]) . eq S [[E1 <= E2]] = (S [[E1]]) <= (S [[E2]]) . eq S [[E1 < E2]] = (S [[E1]]) < (S [[E2]]) . eq S [[not T1]] = not(S [[T1]]) . eq S [[T1 and T2]] = (S [[T1]]) and (S [[T2]]) . eq S [[T1 or T2]] = (S [[T1]]) or (S [[T2]]) . eq S ; X1 := E1 [[X1]] = S [[E1]] . cq S ; X1 := E1 [[X2]] = S [[X2]] if X1 =/= X2 . eq S ; X1 := E1 [[AV]] = S [[AV]] . eq S ; AV[E1] := E2 [[AV]] = (S[[AV]])[ S[[E1]] <- S[[E2]] ] . cq S ; AV[E1] := E2 [[AV']] = S [[AV']] if AV =/= AV' . eq S ; AV[E1] := E2 [[X1]] = S [[X1]] . endth *** extended programming language *** obj PGM is pr BPGM . sort Pgm . subsort BPgm < Pgm . op skip : -> Pgm . op _;_ : Pgm Pgm -> Pgm [assoc prec 50] . op if_then_else_fi : Tst Pgm Pgm -> Pgm [prec 40] . op while_do_od : Tst Pgm -> Pgm [prec 40] . endo obj SEM is pr PGM . pr STORE . sort EStore . subsort Store < EStore . op _;_ : EStore Pgm -> EStore [prec 60] . var S : Store . var T : Tst . var P1 P2 : Pgm . eq S ; skip = S . eq S ; (P1 ; P2) = (S ; P1) ; P2 . cq S ; if T then P1 else P2 fi = S ; P1 if S[[T]] . cq S ; if T then P1 else P2 fi = S ; P2 if not(S[[T]]) . cq S ; while T do P1 od = (S ; P1) ; while T do P1 od if S[[T]] . cq S ; while T do P1 od = S if not(S[[T]]) . endo