EECS 843

Programming Langauge Foundation II


Errata March 22

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.