-
Notifications
You must be signed in to change notification settings - Fork 0
/
examples.why
122 lines (90 loc) · 3.38 KB
/
examples.why
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
theory ValidityTests
use dl.Semantics
(* Example triples tested for validity *)
goal TestValidTripleSimpleProg1 :
let x = MkIdent 0 in
let y = MkIdent 1 in
let prog = Sseq (Sassign y (Ebin (Evar y) Oplus (Econst 10))) Sskip in
let p = Fcomp (Evar y) BOeq (Evar x) in
let q = Fcomp (Evar y) BOeq (Ebin (Evar x) Oplus (Econst 10)) in
validUT p Uskip prog q
goal TestValidTripleSimpleProg2 :
let x = MkIdent 0 in
let y = MkIdent 1 in
let prog = Sseq (Sassign y (Ebin (Evar y) Oplus (Econst 10))) Sskip in
let p = Fcomp (Evar y) BOeq (Evar x) in
let q = Fcomp (Evar y) BOeq (Ebin (Evar x) Oplus (Econst 10)) in
validUT p Uskip prog q
goal TestValidTripleSwapProg :
let x = MkIdent 0 in
let y = MkIdent 1 in
let t = MkIdent 2 in
let a = MkIdent 3 in
let b = MkIdent 4 in
let swap = Sseq (Sassign t (Evar x))
(Sseq (Sassign x (Evar y))
(Sassign y (Evar t))) in
let p = Fand (Fcomp (Evar x) BOeq (Evar a)) (Fcomp (Evar y) BOeq (Evar b)) in
let q = Fand (Fcomp (Evar y) BOeq (Evar a)) (Fcomp (Evar x) BOeq (Evar b)) in
validUT p Uskip swap q
goal TestValidTripleAltSwapProg :
let x = MkIdent 0 in
let y = MkIdent 1 in
let t = MkIdent 2 in
let a = MkIdent 3 in
let b = MkIdent 4 in
let swap = Sseq (Sseq (Sassign t (Evar x))
(Sassign x (Evar y)))
(Sassign y (Evar t)) in
let p = Fand (Fcomp (Evar x) BOeq (Evar a)) (Fcomp (Evar y) BOeq (Evar b)) in
let q = Fand (Fcomp (Evar y) BOeq (Evar a)) (Fcomp (Evar x) BOeq (Evar b)) in
validUT p Uskip swap q
end
theory InferenceTests
use dl.SystemDL
(* Example inferences *)
goal TestInfSimpleProg0 :
let x = MkIdent 0 in
let y = MkIdent 1 in
let p = Fcomp (Evar y) BOeq (Evar x) in
infUT Ftrue Uskip (Sassign x (Evar y)) p
goal TestInfSimpleProg1 :
let x = MkIdent 0 in
let y = MkIdent 1 in
let prog = Sseq (Sassign y (Ebin (Evar y) Oplus (Econst 10))) Sskip in
let p = Fcomp (Evar y) BOeq (Evar x) in
let q = Fcomp (Evar y) BOeq (Ebin (Evar x) Oplus (Econst 10)) in
infUT p Uskip prog q
goal TestInfSimpleProg2 :
let x = MkIdent 0 in
let y = MkIdent 1 in
let prog = Sseq (Sassign y (Ebin (Evar y) Oplus (Econst 10))) Sskip in
let p = Fcomp (Evar y) BOeq (Evar x) in
let q = Fcomp (Evar y) BOeq (Ebin (Evar x) Oplus (Econst 10)) in
infUT p Uskip prog q
goal TestInfSwapProg :
let x = MkIdent 0 in
let y = MkIdent 1 in
let t = MkIdent 2 in
let a = MkIdent 3 in
let b = MkIdent 4 in
let swap = Sseq (Sassign t (Evar x))
(Sseq (Sassign x (Evar y))
(Sseq (Sassign y (Evar t))
Sskip)) in
let p = Fand (Fcomp (Evar x) BOeq (Evar a)) (Fcomp (Evar y) BOeq (Evar b)) in
let q = Fand (Fcomp (Evar y) BOeq (Evar a)) (Fcomp (Evar x) BOeq (Evar b)) in
infUT p Uskip swap q
goal TestInfAltSwapProg :
let x = MkIdent 0 in
let y = MkIdent 1 in
let t = MkIdent 2 in
let a = MkIdent 3 in
let b = MkIdent 4 in
let swap = Sseq (Sseq (Sassign t (Evar x))
(Sassign x (Evar y)))
(Sassign y (Evar t)) in
let p = Fand (Fcomp (Evar x) BOeq (Evar a)) (Fcomp (Evar y) BOeq (Evar b)) in
let q = Fand (Fcomp (Evar y) BOeq (Evar a)) (Fcomp (Evar x) BOeq (Evar b)) in
infUT p Uskip swap q
end