A7a

[Rafiq Shivji]

For the verification conditions, it looks like we need to use the fact
that x=2x, but I'm not sure how to do that. Can we just use it since it
is a line in the code, or should it be part of the preconditions or
something? Or should we just introduce x as a constant?

Thanks,
Rafiq.

[Nancy Day]

Post by Rafiq Shivji
For the verification conditions, it looks like we need to use the fact
that x=2x, but I'm not sure how to do that. Can we just use it since it
is a line in the code, or should it be part of the preconditions or
something? Or should we just introduce x as a constant?

You can't change the precondition or postcondition of the program given
in the question.

You may assert any wff you want at different points in the program
as long as you can justify the assertion with proof rules and verification
conditions.

The premise and conclusion of the verification condition must come from
the annotated program (i.e., you can't add other information to do these
proofs).

cheers, nancy
--------------------------------------------------------------------
Nancy Day, Associate Professor
CS245 Winter 2009 Instructor
http://www.student.cs.uwaterloo.ca/~cs245
David R. Cheriton School of Computer Science, University of Waterloo