I'm working my way through Leino's "Program Proofs" and I was following as far as the semantics of variable assignment, but I'm not quite sure why this is a valid Hoare triple:

{forall x::Q} var x; {exists x :: P}

where P is the weakest precondition and Q is the strongest postcondition. I'm not following why allocating x guarantees that there exists an x that satisfies P.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.