blob: 54668f2e330947b9cd197c22c8d28f3fc3e28dfd (
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
|
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 (seq sqrt st)
Start = toString (tree sqrt st)
where
st :: Var -> Int
st 'x' = 9
|
