22C:123

 

Semantics of a Simple Imperative Programming Language

 

----------------------------------------------------------------------------

The following OBJ code defines the syntax and semantics of a simple programming language, and includes a correctness proof of a program to compute powers. This example is taken from a course on Algebraic Semantics of Imperative Programs taught by Joseph Goguen and Grant Malcolm (see their book on our reserve list).

----------------------------------------------------------------------------

 

obj NAT is sort Nat .

  op 0 : -> Nat .

  op s_ : Nat -> Nat [prec 1] .

endo

 

obj NATOPS is pr NAT .

  op 1 : -> Nat .

  eq 1 = s 0 .

 

  op _+_ : Nat Nat -> Nat [assoc comm prec 3] .

  vars M N : Nat .

  eq  M + 0  =  M .

  eq  M + s N  =  s(M + N) .

 

  op _*_ : Nat Nat -> Nat [assoc comm prec 2] .

  eq  M * 0  =  0 .

  eq  M * s N  =  M * N + M .

 

  op _**_ : Nat Nat -> Nat [prec 4] .

  eq  M ** 0  =  1 .

  eq  M ** s N  =  (M ** N) * M .

 

  op _-_ : Nat Nat -> Nat .

  eq  M - 0  =  M .

  eq  0 - M  =  0 .

  eq  s M - s N  =  M - N .

 

  op _%2 : Nat -> Nat [prec 10] .

  eq  0 %2  =  0 .

  eq  s 0 %2  =  0 .

  eq  s s N %2  =  s(N %2) .

 

  op even_ : Nat -> Bool  [prec 10] .

  eq  even 0  =  true .

  eq  even s 0  =  false .

  eq  even s s M  =  even M .

 

  op pos_ : Nat -> Bool .

  eq  pos 0  =  false .

  eq  pos s N  =  true .

 

  [lemma1] cq (N * N)**(M %2) = N ** M if even M .

  [lemma2] cq N *(N **(M - s 0)) = N ** M if pos M .

endo

 

th STORE is pr NATOPS .

            pr BOOL .

            pr QID *(sort Id to Var) .

  sort Store .

  op initial : -> Store .

  op _[[_]] : Store Var -> Nat .

  op (_;_:_) : Store Var Nat -> Store .

 

  vars X Y : Var .

  var S : Store .

  var N : Nat .

 

  eq  initial [[X]]  =  0 .

  eq  S ; X : N [[X]]  =  N .

  cq  S ; X : N [[Y]]  =  S[[Y]] if X =/= Y .

endth

 


obj EXP is pr STORE .

  sorts Exp Bexp .

  subsorts Nat Var < Exp .

  subsorts Bool < Bexp .

 

  op _*_ : Exp Exp -> Exp .

  op _-_ : Exp Exp -> Exp .

  op _%2 : Exp -> Exp .

  op even_ : Exp -> Bexp .

  op pos_ : Exp -> Bexp .

 

  op _[[_]] : Store Exp -> Nat .

  op _[[_]] : Store Bexp -> Bool .

 

  var S : Store .

  var N : Nat .

  var B : Bool .

  vars E E' : Exp .

 

  eq  S[[N]]  =  N .

  eq  S[[E * E']]  =  S[[E]] * S[[E']] .

  eq  S[[E - E']]  =  S[[E]] - S[[E']] .

  eq  S[[E  %2]]   =  S[[E]] %2 .

 

  eq  S[[B]]  =  B .

  eq  S[[even E]]  =  even(S[[E]]) .

  eq  S[[pos E]]   =  pos(S[[E]]) .

endo

 


obj PGM is pr EXP .

           ex STORE .

  sort Pgm .

 

  op _:=_ : Var Exp -> Pgm .

  op _;_ : Pgm Pgm -> Pgm [assoc prec 50] .

  op if_then_else_fi : Bexp Pgm Pgm -> Pgm .

  op while_do_od : Bexp Pgm -> Pgm .

 

  op _;_ : Store Pgm -> Store .

 

  var S : Store .

  var X : Var .

  var E : Exp .

  var BX : Bexp .

  vars P P' : Pgm .

 

  eq  S ; (X := E)  =  S ; X : S[[E]] .

  eq  S ; (P ; P') =  (S ; P); P' .

  eq  S ; if BX then P else P' fi  =  if S[[BX]]

                                      then  S ; P

                                      else  S ; P'  fi .

  eq  S ; while BX do P od  =  if S[[BX]]

                               then  S ; P ; while BX do P od

                               else  S  fi .

endo

 


***> the program:

obj POW is inc PGM .

  ops a0 b0 : -> Nat .

 

  let init  = 'A := a0 ; 'B := b0 ; 'C := 1 .

  let step  = 'B := 'B - 1 ; 'C := 'C * 'A .

  let inner = 'A := 'A * 'A ; 'B := 'B %2 .

  let outer = while even 'B do inner od ; step .

  let pow   = init ; while pos 'B do outer od .

endo

 

red pow .

 

***> example:

open POW .

eq a0 = s s 0 .

eq b0 = s s s 0 .

red initial ; pow [['C]] .  ***> should be: 8

close

 


***> the verification:

openr POW .

 

***> the invariant:

op inv : Store -> Bool .

var S : Store .

eq  inv(S)  =  ((S[['A]]) ** (S[['B]])) * (S[['C]]) == a0 ** b0 .

 

***> init

op s : -> Store .

red inv(s ; init).  ***> should be: true

 

ops a b c : -> Nat .

eq s[['A]] = a .

eq s[['B]] = b .

eq s[['C]] = c .

close

 

open POW .

eq (a ** b)* c = a0 ** b0 .

eq pos b = true .

eq even b = true .

red inv(s ; inner).  ***> should be: true

close

 

open POW .

eq (a ** b)* c = a0 ** b0 .

eq even b = false .  ***> therefore [lemma3]:

eq pos b = true .

red inv(s ; step) .  ***> should be: true

close