What is the relationship between cycle invariant and weakest precondition
Given the loop invariant, Wikipedia lists, a good way to create weak prerequisites 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] replaces all occurrences of x in M with N.
Now my problem is variable y. \ Forall y binds y in expression, so "y is fresh variable set" doesn't parse for me. Is y bound in \ forall the same as y in "[x <- y]"? I just can't make out the above.
Edit: To rephrase to avoid asking for a link.
My question is: what is the direct relationship between loop invariants and the computation of weak preconditions, if any. It seems that much in practice softens the weak preconditions for loops to a precondition that is suitable for testing. The above from wikipedia suggests that given the loop invariant, one can actually compute the weakest prerequisites on the nose, but I have a hard time understanding this condition.
source to share
The syntax "x <- y" in the rule you quoted means concurrent substitution of multiple variables that we can think of as named x 1, x 2, ... x n respectively, other variables y 1, y 2, ... y nwhich, as you indicate, are directly related in the formula by the formula a \ forall.
The way to apply the rule in practice is to select a set of variables that appear in the predicate R
. The number and name of these variables is left to the choice of the person who applies the rule, but it must be possible to determine a reasonable relationship <
between the tuples of the chosen arity to \forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y]
be ultimately provable.
This is what the wikipedia article means when it says, "At its weakest, the while-loop precondition is usually parameterized by a predicate I
called a loop invariant, and a well-reasoned relationship to the spatial state denoted by <
, and called a loop variant." It is not just I
that it should have been chosen in advance and should decorate the program, there is also a selection of a number of program variables modified in the body of the loop S
and appearing in the condition E
, and the existence of a reasonable order <
between the tuples of values of these variables ensures that the condition E
will ultimately be false.
This is much easier to understand with real validation systems in which you can try something. Read this tutorial to Section 2.3 Checking Completion and see if a practical version of the same explanation makes sense.
source to share