Up
Go up to Question 3

Solution

arprove(Body,E1,E2) is true if the Body can be proved with initial environment E1 and resulting environment E2. The only CILog built-in predicate you can use is >.
arprove(A&B,E1,E3) <-
   arprove(A,E1,E2) &
   arprove(B,E2,E3).
arprove(G,E1,E2) <-
   (G <= B) &
   arprove(B,E1,E2).
arprove(true,E,E).
arprove((V is Exp),E1,E1) <-
   eval(Exp,V,E1).
arprove(assign(X,Exp),E1,E2) <-
   eval(Exp,Val,E1) &
   update(X,Val,E1,E2).
arprove(X > Y,E1,E1) <-
   eval(X,XV,E1) &
   eval(Y,YV,E1) &
   XV > YV.

David Poole

Up