Quiz 11 - Loop Invariant

CS 152 - Spring 2008

Name:

Student ID:

E-mail:

Loop Invariant and Post Condition

Assume an array, A, declared with index bounds 1..n.

The loop invariant, INV, for the program below is given as,

forall x in 1..i,  (A[1] >= A[x])

The post condition, POST, for the program is given as,

forall x in 1..n,  (A[1] >= A[x])

The Program Code

assert (PRE)

i=1

assert (INV)
while (GUARD) do
  assert (INV)
  i = i + 1
  if (A[i] > A[1])  then
    A[1],A[i] = A[i],A[1]
  end
  assert (INV)
end
assert (INV)

assert (POST)

Please Answer and Show All Work

(A) What is the precondition, PRE?

(B) What is the GUARD?