What is the relationship between loop invariant and weakest precondition

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.

The syntax “x <- y” in the rule that you quote means the simultaneous substitution of several variables that we can assume to be named x₁, x₂, … x_n respectively by other variables y₁, y₂, … y_n 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.