In the classical IMP language, the definition of weakest precondition is:

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t"

This is stating that from state s, after executing c we get to a state satisfying Q. My question comes when handling the selection construct in the language of guarded commands (see selection command in Wikipedia). My guess is that in this case one needs to define:

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ (∀ t'. (c,s) ⇒ t' ⟶ Q t)"

I wonder if this is correct. Currently, I'm having problems proving the weakest precondition definition for the sequential composition of commands:

"wp (c1;;c2) Q s = wp c1 (wp c2 Q) s" 

So, I'm beginning to think my definition is wrong.

Does anybody see what am I doing wrong?

  • $\begingroup$ Yes this is correct; this is how things must be defined even for languages with "extremely mild non-determinism" (like heap allocation without a defined allocator). The left conjunct is only necessary if you intend to only allow terminating programs. $\endgroup$ – jozefg Jan 3 at 17:22
  • $\begingroup$ @jozefg my conclusion up to know is that I need a stronger property, in fact I need to state that all possible executions are terminating otherwise the rule for sequential composition wont be stablished $\endgroup$ – Javier Jan 3 at 22:40

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.