[ 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