Logic Web Tutor: Right Answer

Correct Answer.

The program P:

x = y;
if (x < z) { x = z; }

satisfies the Hoare triple

x < y

x = y

with respect to the partial correctness relation

_par since we have the proof

 y < z 		 		   	        Precondition
 (y < z  z = z)  ( (y < z)  y = z)	 Implied
x = y;
(x < y  z = z)  (  (x < z)  z = z)	 Assignment
if (x < z)
	z = z					If-Statement
	x = z;
	x = z					Assignment
x = z						If-Statement

Notice that this proof uses the modified proof rule for the if-statement, although the else-branch is not even present.

Can you modify and simplify our proof rule for if-statements that have no else-branch?
Can you explain why the instance of the proof rule "Implied" above is legitimate?

Back to Question.
Next Question.