-1
$\begingroup$

Does the following program $P$:

a = 2 
b = a + 3
c = a * b

Satisfy the following formula? $$\{ \top \} \; P \; \{ a < (b - 2) + c \}$$

I want to use integers in $P$. The postcondition is satisfied, right?

$\endgroup$
  • 1
    $\begingroup$ We discourage "please check whether my answer is correct" questions, as only "yes/no" answers are possible, which won't help you or future visitors. See here and here. Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher. $\endgroup$ – David Richerby Oct 30 '16 at 17:32
0
$\begingroup$

Using only two properties of the weakest precondition (wp), we can prove this correct as follows.

   wp(a ≔ 2 ; b ≔ a + 3 ; c ≔ a * b ,  a < b - 2 + c )
≡⟨ wp on sequence ⟩
   wp(a ≔ 2 , wp (b ≔ a + 3 , wp (c ≔ a * b , a < b - 2 + c)))
≡⟨ wp on assignment ⟩
   wp(a ≔ 2 , wp (b ≔ a + 3 , a < b - 2 + a * b))
≡⟨ wp on assignment ⟩
   wp(a ≔ 2 , a + 3 < a + 3 - 2 + a * (a + 3))
≡⟨ wp on assignment ⟩
   2 + 3 < 2 + 3 - 2 + 2 * (2 + 3)
≡⟨ arithemtic ⟩
   5 < 13
≡⟨ arithemtic ⟩
   true

Hence,

{ true }   a ≔ 2 ; b ≔ a + 3 ; c ≔ a * b   { a < b - 2 + c }
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.