module test

import While

from StdMisc import abort
from StdOverloaded import class +++(..), class toString(..)
from StdString import instance +++ {#Char},
        instance toString Char, instance toString Int
import _SystemArray

// From http://www.cs.ru.nl/~hubbers/courses/sc/leertaak/04.html
// The rounded down square root function:
//  { x=n /\ n >= 0 } sqrt { z^2 <= n /\ (z+1)^2 > n }
sqrt :: Stm
sqrt = 'z' := 0 :.
       'o' := 1 :.
       's' := 1 :.
       While ('s' <= 'x')
         ( 'z' := 'z' + 1 :.
           'o' := 'o' + 2 :.
           's' := 's' + 'o' )

Start = toString (tree sqrt st)
where
    st :: Var -> Int
    st 'x' = 16