diff options
Diffstat (limited to 'test.icl')
| -rw-r--r-- | test.icl | 23 |
1 files changed, 13 insertions, 10 deletions
@@ -1,6 +1,7 @@ module test import While +from WhileVars import o, s, x, z from StdMisc import abort from StdOverloaded import class +++(..), class toString(..) @@ -12,18 +13,20 @@ import _SystemArray // 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' ) +sqrt = z := 0 :. + o := 1 :. + s := 1 :. + While (s <= x) + ( z := z + 1 :. + o := o + 2 :. + s := s + o ) -//Start = toString (seq sqrt st) -Start = toString (tree sqrt st) +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 where - st :: Var -> Int + st :: Char -> Int st 'x' = 9 |