blob: 7d5a11876c721290601bf53d48e2ef81fea96995 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
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
|
