3

Given a loop invariant, Wikipedia lists, a nice way to produce the weakest preconditions for a loop (from http://en.wikipedia.org/wiki/Predicate_transformer_semantics):

wp(while E inv I do S, R) = 
    I \wedge
    \forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] \wedge
    \forall y. ((\neg E \wedge I) \implies R)[x <- y]
where y is a tuple of fresh variables.

M[x <- N] substitutes all the occurrences of x in M with N.

Now, my problem is the variable y. The \forall y, binds y in the expression, so "y is a tuple of fresh variables" doesn't parse for me. Is the y bound in the \forall, the same as the y in "[x <- y]"? I simply cannot parse the above.

Edit: Rephrased to avoid reference request.

My question is: what the direct connection between loop invariants and computing weakest preconditions, if any. It seems a lot of things done in practice relax weakest precondition for loops to a precondition that is suitable for verification. The above from wikipedia suggests that given a loop invariant, one can indeed compute the weakest preconditions on the nose, but I am having trouble understanding this condition.

Jove
  • 33
  • 4

1 Answers1

1

The syntax “x <- y” in the rule that you quote means the simultaneous substitution of several variables that we can assume to be named x1, x2, … xn respectively by other variables y1, y2, … yn which, as you point out, are bound immediately above in the formula by a \forall.

The way to apply the rule in practice is to pick a set of variables occurring in the predicate R. The number and the name of these variables is left to the choice of the person who applies the rule, but it must be possible to define a well-founded relation < between tuples of the chosen arity such that \forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] will be provable eventually.

This is what the wikipedia article means when it says “Weakest-precondition of while-loop is usually parametrized by a predicate I called loop invariant, and a well-founded relation on the space state denoted < and called loop variant.” It is not just I that must have been chosen in advance and must decorate the program, there is also the choice of a number of variables of the program modified in the body of the loop S and occurring in the condition E, and the existence of the well-founded order < between the tuples of values of these variables guarantee that the condition E is false eventually.

This is much easier to understand with actual verification systems in which it is possible to try out things. Read this tutorial up to section 2.3 Checking Termination and see if the practical version of the same explanation makes more sense to you.

Pascal Cuoq
  • 79,187
  • 7
  • 161
  • 281
  • Thank you very much for the response. I am still a bit confused; if I substitute y for x in an expression, which contains, among other things, "x < y" then I will get "y < y" which should never be true. – Jove Oct 14 '14 at 20:41
  • @Jove wp(…) is not a logic function. You cannot substitute inside its arguments. It is a meta-function (that takes logic terms as arguments). – Pascal Cuoq Oct 14 '14 at 20:45
  • Thank you. Can I say the following: first obtain wp(S, I \wedge x < y), call this T, and then substitute y for x in ((E \wedge I) \implies T), so that x and y are both bound by the \forall y... ? – Jove Oct 14 '14 at 21:24
  • @Jove Yes, you can say that. – Pascal Cuoq Oct 14 '14 at 21:52
  • Could you guys please give a simple example of how you manage to make these textual substitions for a loop ? I have such an exercise to solve and I'm nearly desperate. Thanks in advance. – Ilian Vasilev Kulishev May 27 '16 at 22:51