Axiomatic Semantics - How to calculate a weakest precondition of a program

Question

Assuming the post-condition, how can I compute the weakest pre-condition of a program containing two statements?

For example :

 a=x;
 y = 0 
 {x = y + a}

Another example:

  y = x;
  y = x + x + y 
  {y = 3x ^ z> 0}

I tried to solve them but both questions resulted in pre-conditions or post-condition that are identical to the statement and I don't know if this is valid.

for example, the precondition of the last statement is "y=x" , thus it is the post condition of the preceding statement which is " y=x" as well

Answer 1

You can apply the rules of Hoare Logic here. Specifically, for the examples you have, you only need the rule for assignment:

---

{ P[E/x] } x = E { P }

Here, P[E/x] means take P and substitute (i.e. replace) all occurrences of x with E. For example, if P is x == 0 then P[0/x] gives 0 == 0.

To calculate the weakest precondition, you start from the end and work backwards. For your first example, we start with the last statement:

{ ??? } y = 0 { x == y + a }

The goal is to determine something suitable for ???. Applying our rule for assignment above, we can see that this is a solution:

{ x == 0 + a } y = 0 { x == y + a }

We can further simplify this to { x == a }. Then, we move on to address the statement before y = 0, and so on.