n = 999
x = 999
i = 0
sum = 0
"""{
     1.OK i == 0  premise
     2.OK sum == 0 premise
     3.OK  sum == x * i  algebra 2 1
     4.OK n == 999  premise
     5.OK return 3 4
}"""
while i != n :
    """{ invariant sum == x* i  modifies i sum }"""
    sum = sum + x
    """{
     1.OK sum == sum_old + x  premise
     2.OK  sum_old  == x * i     premise
     3.OK  sum == (x*i) + x      algebra 2 1
    }"""
    i = i + 1
    """{
     1.OK i == i_old + 1  premise
     2.OK sum == (x * i_old) + x   premise
     3.OK sum == x * (i_old + 1)   algebra 2
     4.OK sum == x * i     subst 1 3
     5.OK sum == x * i  subst 1 3
    }"""

"""{ 1.OK sum == x* i  premise
     2.OK  not ( i != n)   premise
     3.OK  i == n       algebra 2
     4.OK  sum == x * n   subst 3 1
}"""