C++ Loop Invariant

C++ Loop Invariant

Loop invariants are critical tools for the proof of correctness of algo-
rithms; they represent the “inductive step” in a proof by induction that
the configuartion of the variables satisfies certain conditions throughout the
algorithm.
To formalize this concept, we introduce some terminology.
Let x1, . . . , xm denote the variables on which an algorithm operates;
let Ai be the domain of xi (set of possible values of xi). A configuration
a = (a1, . . . , am) is an assignment of values to each variable (ai ∈ Ai). The
set of all conceivable configurations is C = A1 × . . . × Am; we call C the
configuration space. A feasible configuration is a configuration which can
actually occur in the course of an execution of the algorithm. Note that in
general, not all configurations are feasible.

Example: the variables in Dijkstra’s algorithm are the priority queue L and
for each vertex i ∈ V , the variables status(i), c(i), and p(i) (the current
status, cost, and parent of vertex i), a total of 3n + 1 variables where n is
the number of vertices. The domain of status(i) is {white, grey, black }; the
domain of c(i) is R+ ∪{∞} (the nonnegative reals and infinity); the domain
of p(i) is V ∪ {NIL }. The domain of L can be thought of as 2V (the set of
all subsets of V ).
An example of an infeasible configuration that nevertheless belongs to
the configuration space is a configuration where some vertex i belongs to
the queue while status(i) =black.

A predicate over C is a function P : C → {0, 1} where 0 indicates “FALSE”
and 1 indicates “TRUE.” A transformation of C is a function S : C → C.
If P is a predicate and a ∈ C a configuration then instead of writing
P(a) = 1, we just write “P(a),” meaning “the statement P(a) is TRUE”;
i. e., the configuration a satisfies the predicate P. For P(a) = 0 we may
write “¬P(a),” meaning the negation of P(a) holds, i. e., a does not satisfy
P. In other words, P is false on a.
The effect of a sequence S of instructions in the code is a change of the
values of the variables and therefore S can be thought of as a transformation
S : C → C.

Definition. Let P and Q be predicates over the configuration space and
let S be a sequence of instructions, viewed as a transformation of the con-
figuration space. Consider the loop
while P do S.
We call Q a loop-invariant for this loop if for all configurations a it is true
that
(∀a ∈ C)( if P(a)&Q(a) then Q(S(a))).

Algorithm:

GetMiddle (List l){
pSlow = pFast = l;
while ((pFast->next)&&(pFast->next->next)){
pFast = pFast->next->next
pSlow = pSlow->next
}
return pSlow
}

#include
#include

int main()
{
int n, min;
cout<<"Masukkan bilangan positif(0 untuk selesai): "; cin>>n;
for(min=n;n>0;)
{
if(n>n;
}
cout<<"min = "< getch();
return 0;
}