File: isqrt_fun.py

package info (click to toggle)
why3 1.8.2-3
  • links: PTS, VCS
  • area: main
  • in suites:
  • size: 45,028 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (16 lines) | stat: -rw-r--r-- 367 bytes parent folder | download | duplicates (6) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 

# 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