Say state variables are (without loss of generality). Now suppose assignment is (wlog). Let:
Suppose an input state vector satisfies , so satisfies , so is True . Now set , so output vector is . Then is True . So this shows equation is correct.
Is as general as possible? Need to show any input to the assignment that satisfies the postcondition must also satisfiy the precondition. Put another way, we need to show that if the precondition is not satisfied, nor can the postcondition be.
So say is False . Then letting , the output of the assignment given input is , and of course , which is False .
David Goodwin 2008-09-20