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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
|
# CleanWhile
Clean While tools
This module provides types and tools to work with [While][while] in
[Clean][clean]. Features include:
- Types for While statements, arithmetic and boolean expressions, states,
derivation trees and derivation sequences
- semi-prettyprint `toString` for those types
- Evaluating statements in states
- Constructing derivation trees and sequences according to the rules of
Natural and Structural Operational Semantics as defined by [Nielson &
Nielson][wiley]
## Example: square root
For example, the [following program][sqrt] is a rounded down square root
function (if `x=n` at the start and `n` is a natural number, then `z` is the
square root of `n`, rounded down, after execution):
import While
from WhileVars import o, s, x, z // o :== Var 'o'; etc.
sqrt :: Stm
sqrt = z := 0 :.
o := 1 :.
s := 1 :.
While (s <= x)
( z := z + 1 :.
o := o + 2 :.
s := s + o )
### Evaluation
We can now execute this code on a `State`, which maps `Var` to `Int`:
Start :: Int
Start = eval NS sqrt st z
where
st :: Char -> Int // Or: st :: Var -> Int // st :: CharState
st 'x' = 9 // st (Var 'x') = 9 // st = \'x' -> 9
`eval NS sqrt st` is a `State` itself (the state that results from execution of
`sqrt` in `st`), so we apply that to `z` to get the result. Other than the
[documentation of While][while] suggests, a `State` can be a partial function
here. There is no efficient way of enforcing total functions in Clean.
The `NS` argument tells the module to use Natural Semantics (as opposed to
`SOS`, Structural Operational Semantics). The result should be the same (though
this has not been heavily tested, it has been proven for the derivation rules
that define NS and SOS, and the functions in this module are directly derived
from those rules). These two semantics are defined for While by Nielson and
Nielson in [Semantics with Applications: A Formal Introduction][wiley].
### Constructing derivation trees and sequences
Besides evaluating statements, we can also construct derivation trees and
sequences. The following two Start rules generate a derivation tree for Natural
Semantics and a derivation sequence for Structural Operational Semantics. Both
types can be `toString`ed:
Start = tree sqrt st
Start = seq sqrt st
For example, the tree for `sqrt` in `st` with `st x = 9` (when passed to
`toString`):
(z:=0; o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
z:=0
(o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=1
(s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=1
(while s<=x do (z:=z+1; o:=o+2; s:=s+o)
(z:=z+1; o:=o+2; s:=s+o
z:=z+1
(o:=o+2; s:=s+o
o:=o+2
s:=s+o
)
)
(while s<=x do (z:=z+1; o:=o+2; s:=s+o)
(z:=z+1; o:=o+2; s:=s+o
z:=z+1
(o:=o+2; s:=s+o
o:=o+2
s:=s+o
)
)
(while s<=x do (z:=z+1; o:=o+2; s:=s+o)
(z:=z+1; o:=o+2; s:=s+o
z:=z+1
(o:=o+2; s:=s+o
o:=o+2
s:=s+o
)
)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
)
)
)
)
)
)
And the sequence:
z:=0; o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=1; s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=1; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)
while s<=x do (z:=z+1; o:=o+2; s:=s+o)
if s<=x then (z:=z+1; o:=o+2; s:=s+o; while s<=x do (z:=z+1; o:=o+2; s:=s+o)) else skip
skip
As you can see, neither method outputs the states. Since a `State` is actually
a function (and not a `[(Var, Int)]`, for example), it is impossible to
`toString` a `State` *an sich*. It *may* be possible to `toString` states in
the context of a derivation tree or sequence, by looking for the variables
present or modified. This is something for a next version.
## Warning
This breaks `StdEnv` completely. Only import what you need, as always, and use
qualified imports where needed.
## Todo
- Gast testing
- Prettyprint for `DerivTree`
- Parser
- Add the state to the `toString` of `DerivTree` and `DerivSeq`
- Easy interface for While language extensions
## Copyright & license
Copyright © 2016 Camil Staps. Licensed under MIT, see LICENSE.
[while]: http://profs.sci.univr.it/~merro/files/WhileExtra_l.pdf
[clean]: http://clean.cs.ru.nl/Clean
[wiley]: http://cs.ioc.ee/~tarmo/pls06/wiley.ps.gz
[sqrt]: http://www.cs.ru.nl/~hubbers/courses/sc_1516/leertaak/04.html
|
