Cycle Invariant Explanation

Question

This is a question from a past exam paper.

Why does the loop invariant say i<=n when the loop test says i<n .

Is there a suitable answer: it says i<=n , how i will be equal to n in the failure condition in the while loop. Therefore, the 6th iteration i will be equal to the value of n 6 in the failure condition. However, the while loop itself points to i<n , since i starts at 0 and ends the cycle once i equals 5.

 private int n =6; public int fact(){ int i = 0; int f = 1; /**loop invariant * 0<=i<=n * f=i! */ while(i<n){//loop test i=i+1; f=f*i; } return f; } 

Answer 1

Because Post-Condition is i==n when the loop remains. Pre-Condition when entering i==0 loop. Inside the loop, i counted towards n . Thus, the invariant 0 <= i <= n .

I have omitted the invariant parts for f in my exlanation. This is not enough, since the invariant should fix the correctness and meaning of the cycle.

 private int n = 6; public int fact(){ int i = 0; int f = 1; /* loop invariant: 0 <= i <= n && f == i! */ /* PRE: i == 0 && f == i! */ while (i < n) { i = i + 1; f = f * i; } /* POST: i == n && f == i! */ return f; } 

Answer 2

A loop invariant is a condition that must be true during each iteration of the loop. In this example, we will consider what are the possible values ​​of the variable i . When the cycle begins, the value of i is 0. At the last iteration of the cycle, i increases by n at the beginning of the cycle, and then another calculation is performed. Therefore, the value of i satisfies the condition 0<=i<=n during the execution of this cycle.

Answer 3

At the last iteration of the cycle, i starts at five, and then increases to 6. i<n will not be executed at the end of the final iteration. Remember that loop invariants must be preserved at the beginning (conditional) and at the end (after the last statement) of each iteration.

Also note that this should be 0 <= i <= n, not 0 < i <= n, since 0<i will not take place at the end of the first iteration.