Divisor
Method finding a divisor of an integer; demonstrates for loops and break statements.
from nagini_contracts.contracts import *
def find_divisor_for(product: int) -> int:
Requires(product > 2)
Ensures(Result() >= 2 and Result() <= product)
Ensures(Forall(int, lambda x: (Implies(x >= 2 and x < Result(), product % x != 0), [[product % x]])))
Ensures(Implies(Result() != product, product % Result() == 0))
for i in range(2, product):
Invariant(i >= 2 and i <= product)
Invariant(Forall(Previous(i), lambda x: (product % x != 0, [[product % x]])))
if product % i == 0:
Assert(Previous(i) == ToSeq(range(2, i)))
break
else:
i = product
return i