#!/usr/bin/python

P = [None, 2]

count = 1

# GLOBAL INVARIANTS
#        { GI:
#	   P[0] = NONE /\ 0 < count < n = 1001 /\
#	   Forall j: count < j < n: P[j] = NONE
#	   Forall i: 0 < i <= count: 
#             [P[i] = p_i => p_i is the i-th prime]
#        }

def prime5WRT (P, a, l):
    global count
    iscomposite = False
    # { INV: GI /\ Forall j: 1<= j < !i: a mod P[j] <> 0 }
    # { BF: count - l + 1 = b0 >= 0}
    while (l <= count) and (P[l] <= a // P[l]) and not(iscomposite):
        iscomposite = (a % P[l] == 0)
        l += 1
    # { INV /\ [ a is composite \/
    #		 (l > count) \/ P[l]^2 > a)  /\ a is not composite]}
    return not(iscomposite)

def generate5From (P, m, n, k):
    global count
    # { INV: GI /\ count <= n /\ 
    #            (Forall j: 1<= j <= !count: P[j] < m) /\
    #            (Forall m': P[count] < m' < m: m' is not a prime)
    # }
    # { BF: b0 = n - k + 1 >= 0}
    while k <= n:
        if prime5WRT (P, m, 1):
            P.append (m)
            count = k
            k += 1 # { BF:  n - k + 1 = b0 -1 }
        else:
            pass
        m += 2
     # {INV /\ k > n}
     
def gen1000Primes():
    generate5From (P, 3, 1000, count+1)


def printArray (P):
    global count
    for i in range(1, count+1):
        print 'Prime [', i, '] = ', P[i]

gen1000Primes ()
printArray (P)