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.

To make things official, class on February 25 will start at 11:30 in the Nichols Hall lobby where we will carpool to The Burrito King. If it’s a nice day, we’ll stay there and do some Coq proofs at Burrito King. If it’s not a nice day, we’ll come back to Nichols, hang out, eat burritos, and do proofs. Pretty much geek heaven as far as I’m concerned.

Welcome to the website for EECS 843 - Programming Language Foundations II at the University of Kansas. Please check here frequently for breaking news and information about projects and exams.

This site is hosted on GitHub and constructed using GitHub Pages, Jekyll and Liquid Tags.