module test

import While
from WhileVars import o, s, x, z

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 :: Int                      // Value of z after execution of sqrt in st
Start = eval NS sqrt st z
//Start = toString (seq sqrt st)    // Derivation sequence of sqrt in st
//Start = toString (tree sqrt st)   // Derivation tree of sqrt in st
//Start = toString sqrt             // The statement itself
where
    st :: Char -> Int
    st 'x' = 9