a = [] def square(): """Updates global array a in place so that each of its ints are squared""" """{ pre True post forall 0 <= i < len(a), a[i] == a_in[i] * a_in[i] }""" global a a_in = [ _v for _v in a ] x = 0 """{ 1.OK forall 0 <= _i < len(a), a[_i] == a_in[_i] premise 2.OK forall 0 <= i < len(a), a[i] == a_in[i] substindex 1 3.OK x == 0 premise 4.OK forall x <= i < len(a), a[i] == a_in[i] subst 3 2 5.OK forall 0 <= i < x, a[i] == a_in[i] * a_in[i] foralli 3 6.OK return 4 5 }""" while x != len(a) : """{ invariant (forall 0 <= i < x, a[i] == a_in[i] * a_in[i]) and (forall x <= i < len(a), a[i] == a_in[i]) modifies x, a }""" """{ 1.OK (forall 0 <= i < x, a[i] == a_in[i] * a_in[i]) and (forall x <= i < len(a), a[i] == a_in[i]) premise 2.OK forall 0 <= i < x, a[i] == a_in[i] * a_in[i] ande 1 3.OK forall x <= i < len(a), a[i] == a_in[i] ande 1 4.OK return 2 3 }""" assert x >= 0 # this is actually an invariant assert x < len(a) # this is actually an invariant a[x] = a[x] * a[x] """{ 1.OK a[x] == a_old[x] * a_old[x] premise 2.OK forall 0 <= i < x, a[i] == (a_in[i] * a_in[i]) premise 3.OK forall x <= i < len(a_old), a_old[i] == a_in[i] premise 4.OK a_old[x] == a_in[x] foralle x 3 5.OK a[x] == a_in[x] * a_in[x] subst 4 1 6.OK forall 0 <= i < (x+1), a[i] == (a_in[i] * a_in[i]) foralli 2 5 7.OK forall (x+1) <= i < len(a), a[i] == a_in[i] premise 8.OK return 6 7 }""" x = x + 1 """{ 1.OK forall 0 <= i < (x_old+1), a[i] == (a_in[i] * a_in[i]) premise 2.OK forall (x_old + 1) <= i < len(a), a[i] == a_in[i] premise 3.OK x == x_old + 1 premise 4.OK forall 0 <= i < x, a[i] == (a_in[i] * a_in[i]) subst 3 1 5.OK forall x <= i < len(a), a[i] == a_in[i] subst 3 2 6.OK return 4 5 }""" """{ 1.OK (forall 0 <= i < x, a[i] == (a_in[i] * a_in[i])) and (forall x <= i < len(a), (a[i] == a_in[i])) premise 2.OK not (x != len(a)) premise 3.OK x == len(a) algebra 2 4.OK forall 0 <= i < x, a[i] == (a_in[i] * a_in[i]) ande 1 5.OK forall 0 <= i < len(a), a[i] == (a_in[i] * a_in[i]) subst 3 4 }"""