Please no teamwork for this assignment!
Consider the program (forever C) where:
C = x = (load = 1 -> In1 | x)
y = (load = 1 -> y | not x)
done = (load = 1 -> 0 | 1)
Prove the following temporal statement using the axioms and inference rules
in the book. You may use other axioms and rules if you first show their
soundness:
{ forever C }
IMPLIES Box { done=0 IMPLIES load=0 }
IMPLIES Box ( {load=1 AND In1=a }
IMPLIES DIAMOND { x=a AND y=not a AND done=1 })
Extra: Can you prove a stronger statement?
sabry@cs.uoregon.edu