Blog

After a disastrous lecture, I thought I would create a blog post clarifying some concepts that were discussed. Hopefully this will help and not hurt…

Given predicates `A`

and `B`

, if `A=>B`

we say that `A`

is *stronger* than `B`

and `B`

is *weaker* than `A`

. If `A=>B`

and `B=>A`

, then `A`

and `B`

are isomorphic. This is the definition that I started with before things went downhill.

If `A`

is stronger than `B`

, there may be things that are derivable from `A`

that are not derivable from `B`

. However, there is nothing in `B`

or derivable from `B`

that is not also derivable from `A`

.

A quick example from propositional logic: `X/\Y`

is stronger than `X`

and stronger than `X\/Y`

. `X/\Y`

is also stronger than `Y/\X`

and visa versa.

Now consider `P`

and `P'`

predicates over state. If `forall st, P st => P' st`

, then `P`

is stronger than `P'`

and `P->>P'`

means that `P`

is stronger than `P'`

. The confusion erupts when we think about what this means with respect to programs. Whether we are weakening or strengthening has depends on whether we start with `P`

and choose `P'`

or `P'`

and choose `P`

. If we are reasoning backwards from `Q`

, which is typically the case, we will frequently derive a precondition for `c`

that gives us `Q`

. I think of this as `P'`

. More specifically, if we want `Q`

to result from `c`

, then find a `P'`

that in conjunction with the Hoare rules for `c`

makes `Q`

true. If we use the Hoare logic backwards over `c`

, `P'`

is the weakest precondition that makes `Q`

true.

The consequence rule allows strengthening `P'`

to some `P`

such that:

`P->>P' /\ {P'}c{Q}`

Because `P`

implies `P'`

we can be assured that when `P`

is true, `P'`

is also true. Thus we can have the following rule:

`P->>P' -> {P'}c{Q} -> {P}c{Q}`

which is called the precondition consequence rule.

In summary, you can safely strengthen the precondition to get a precondition that better suits the proof structure.

So why did we get wrapped around the axel in class? It would help if I transcribed from the book a bit better, but the real reason is what strengthening means. When `P`

is stronger than `P'`

it admits fewer states and all those states satisfy `P'`

. With respect to `c`

, that means simply we know states satisfying `P'`

will result in `Q`

, but we’re taking the subset of `P'`

that satisfy `P`

. Effectively, we’re not allowing states we know satisfy `P'`

, the weakest precondition. If we weaken `P'`

all bets are off because `P'`

is weakest.