examples/python/isqrt_fun.py


# same as sqrt.py, but with a function

def isqrt(n):
    #@ requires n >= 0
    #@ ensures  result * result <= n < (result + 1) * (result + 1)
    r = 0
    s = 1
    while s <= n:
        #@ invariant 0 <= r
        #@ invariant r * r <= n
        #@ invariant s == (r+1) * (r+1)
        #@ variant   n - s
        r = r + 1
        s = s + 2 * r + 1
    return r
python: new example 2017-03-09 15:48:55 +01:00
			`# same as sqrt.py, but with a function`

			`def isqrt(n):`
			`#@ requires n >= 0`
			`#@ ensures result * result <= n < (result + 1) * (result + 1)`
			`r = 0`
			`s = 1`
			`while s <= n:`
			`#@ invariant 0 <= r`
			`#@ invariant r * r <= n`
			`#@ invariant s == (r+1) * (r+1)`
python: functions and predicates 2017-03-17 17:04:23 +01:00			`#@ variant n - s`
python: new example 2017-03-09 15:48:55 +01:00			`r = r + 1`
			`s = s + 2 * r + 1`
			`return r`