[ This message contains my replies to two student queries about axiomatic
semantics. ]
Student 1 wrote:
> Hey Wes, i'm a little unclear on the syntax for WP and VC with respect to
> the whole [e/x] thing...
Student 2 wrote:
> What I'd like to do is (1) go over an example of computing a verification
> condition using substitution (e.g., [e/x]) and (2) clarify the notion of
> soundness and completeness with respect to Hoare rules (how would I know
I potentially have free time today at noon; the two of you (and any others)
are welcome to join me for lunch then to talk about this. Stop by my office
just before noon.
Briefly:
> for example: assignment: VC(x:=e, B) = [e/x]B
>
> isn't the right side of the equality supposed to be a precondition?
Yes, [e/x]B is a precondition -- it is also an assertion.
Consider this example:
VC(x := 7 + z, x > 10)
What precondition would have to be true for x>10 to be true *after*
executing x:=7+z? Our intuition says z>3. Let's compute the VC:
VC(x := 7+z, x>10) = [7+z/x](x>10) = 7+z>10 == z>3
Looks good: the VC matches our intuition.
> equation...if that's the case (and i'm correct in thinking [e/x] means x
> is equal to e)
[e/x] means perform capture-avoiding substitution, replacing all instances
of x in the assertion with e. It's the same substitution notation we've been
using in other topics in class.
http://en.wikipedia.org/wiki/First-order_logic#Substitution
Thus [e/x]B is a *new assertion* that looks just like B, except that all
free instances of x have been replaced by copies of e.
> go over an example of computing a verification condition using
> substitution (e.g., [e/x])
Here's a second example:
command c == if x > 10 then y := 2 else y := z
postcondition B == y < 0
If you stare at the command for a bit, you'll see that in order for y to be
negative after executing it, we'll need x<=10 and z<0. Let's see how that
comes out in the VC ...
VC(c,B) = (x>10) => VC(y:=2,B) and (x<=10) => VC(y:=z,B)
= (x>10) => 2<0 and (x<=10) => VC(y:=z,B)
= (x>10) => 2<0 and (x<=10) => z<0
That's officially the VC. But if we do some more logic and simplification:
= (x>10) => false and (x<=10) => z<0
= not (x>10) and (x<=10) => z<0
= x<=10 and (x<=10) => z<0
= x<=10 and z<0
> and (2) clarify the notion of soundness and completeness with respect to
> Hoare rules (how would I know whether a particular rule is sound and/or
> complete?).
A rule is Sound if it can only prove true things.
A rule is Complete if it can prove all true things.
You detect unsoundness or incompleteness by trying some small programs with
preconditions and seeing if you can find a counterexample.
Here is an unsound rule:
---------------------------
|- { true } x := e { B }
(Intuitively, this rule is unsound because it allows us to prove any
postcondition B that we want!) To demonstrate unsoundness, I find an
instance of the command and a postcondition B such that running the command
in a state that satisfies the precondition, and having the command
terminate, does not result in a state that satisfies B.
To demonstrate unsoundness, I will pick c == "x := 5" and B == "x > 10".
Using the rule, we get:
------------------------------
|- { true } x := 5 { x>10 }
So the precondition is true. If I start in a state sigma satisfying true
(which is any sigma!) and execute this command, I'll end up in a state
sigma' where x = 5. But such a state sigma' does *not* satisfy x>10 (since
5>10 is not true), so this rule is unsound.
Here is an incomplete rule:
|- { A } c1 { B } |- { A } c2 { B }
----------------------------------------
|- { A } if e then c1 else c2 { B }
To show that the rule is incomplete, I pick a command c and a postcondition
B and a precondition A such that actually executing the command in a state
sigma that satisfies A, and having the command terminate, causes the
program to terminate in a state that satisfies B *but you can't prove it
with the rule*.
To show that the rule is incomplete, I will pick:
c == if x > 10 then skip else x := 11
B == x > 10
A == true
It is true that executing the command c in any state causes it to terminate
with x>10. However, we won't be able to prove it using that rule. Thus that
rule is incomplete. However, we must detail exactly why we can't prove it.
We can get the second hypothesis (the one involving c2) using the rule of
consequence, but we can't get the first one:
|- {11>10 => true} |- {11>10} x:=11 {x>10}
~~~ fail! ~~~ --------------------------------------------
|- { true } skip { x>10 } |- { true } x:=11 { x>10 }
-------------------------------------------------------------------------
|- { true } if x>10 then skip else x:=11 { x>10 }
There is no way to make a derivation for the left hypothesis, so this rule
is incomplete. Intuitively, the rule is incomplete because it doesn't let
you assume "e" when proving the true branch and it doesn't let you assume
"not e" when proving the false branch: without those extra assumptions you
don't have enough power to prove all true things. So the rule is
incomplete.
- Wes