Newer
Older
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
module WLP.WLPCalculator
( programToWLPAlgebra
)
where
import GCLParser.GCLAlgebra
import WLP.LogicalExpression as LE
import WLP.MathExpression as ME
type BinOp = (MathExpression -> MathExpression -> MathExpression)
-- type ProgramAlgebra pty ty vd stmt expr bo res
programToWLPAlgebra :: ProgramAlgebra () () () (LogicalExpression -> LogicalExpression) MathExpression BinOp LogicalExpression
programToWLPAlgebra =
( program
, variableDeclaration
, ( ptInt
, ptBool
)
, ( ptype
, reftype
, arraytype
)
, ( skip
, assert
, assume
, assign
, aassign
, drefassign
, seq
, ifthenelse
, while
, block
, trycatch
)
, ( var
, liti
, litb
, litnull
, parens
, arrayelem
, opneg
, binopexpr
, forall
, sizeof
, repby
, cond
, newstore
, dereference
)
, ( and
, or
, implication
, lessthan
, lessthanequal
, greaterthan
, greaterthanequal
, equal
, minus
, plus
, multiply
, divide
, alias
)
)
where
program s i o stmt = stmt $ LE.Constant True
variableDeclaration = undefined
ptInt = undefined
ptBool = undefined
ptype = undefined
reftype = undefined
arraytype = undefined
skip = \le -> le
assert me = \le -> Expression me :/\: le
assume me = \le -> Expression me :\/: le
assign var e = \le -> replace var e le
aassign = undefined
drefassign = undefined
seq s1 s2 = \le -> s1 (s2 le)
ifthenelse g s1 s2 = \le -> (Expression g :/\: s1 le) :\/: (Not (Expression g) :/\: s2 le)
while = undefined
block = undefined
trycatch = undefined
var = ME.Variable
liti = ME.Constant
litb = undefined
litnull = undefined
parens = undefined
arrayelem = undefined
opneg = undefined
binopexpr op e1 e2 = op e1 e2
forall = undefined
sizeof = undefined
repby = undefined
cond = undefined
newstore = undefined
dereference = undefined
and = undefined
or = undefined
implication = undefined
lessthan = ME.LT
lessthanequal = ME.LTE
greaterthan = ME.GT
greaterthanequal = ME.GTE
equal = ME.EQ
minus = ME.Sub
plus = ME.Add
multiply = ME.Mul
divide = ME.Div
alias = undefined