Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestPrim.agda @ 3:6be8ee856666

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add simple Hoare logic example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Dec 2018 16:26:49 +0900
parents
children 64bd5c236002
comparison
equal deleted inserted replaced
2:b05a4156da01 3:6be8ee856666
1 module whileTestPrim where
2
3 open import Function
4 open import Data.Nat
5 open import Data.Bool hiding ( _≟_ )
6 open import Level renaming ( suc to succ ; zero to Zero )
7 open import Relation.Nullary using (¬_; Dec; yes; no)
8 open import Relation.Binary.Core
9
10
11
12 record Env : Set where
13 field
14 varn : ℕ
15 vari : ℕ
16 open Env
17
18 PrimComm : Set
19 PrimComm = Env → Env
20
21 Cond : Set
22 Cond = (Env → Bool)
23
24 data Comm : Set where
25 Skip : Comm
26 Abort : Comm
27 PComm : PrimComm -> Comm
28 Seq : Comm -> Comm -> Comm
29 If : Cond -> Comm -> Comm -> Comm
30 While : Cond -> Comm -> Comm
31
32 _-_ : ℕ -> ℕ -> ℕ
33 x - zero = x
34 zero - _ = zero
35 (suc x) - (suc y) = x - y
36
37 lt : ℕ -> ℕ -> Bool
38 lt x y with (suc x ) ≤? y
39 lt x y | yes p = true
40 lt x y | no ¬p = false
41
42 Equal : ℕ -> ℕ -> Bool
43 Equal x y with x ≟ y
44 Equal x y | yes p = true
45 Equal x y | no ¬p = false
46
47 program : Comm
48 program =
49 Seq ( PComm (λ env → record env {varn = 10}))
50 $ Seq ( PComm (λ env → record env {vari = 0}))
51 $ While (λ env → lt (varn env ) zero )
52 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
53 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
54
55 simple : Comm
56 simple =
57 Seq ( PComm (λ env → record env {varn = 10}))
58 $ PComm (λ env → record env {vari = 0})
59
60 {-# TERMINATING #-}
61 interpret : Env → Comm → Env
62 interpret env Skip = env
63 interpret env Abort = env
64 interpret env (PComm x) = x env
65 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
66 interpret env (If x then else) with x env
67 ... | true = interpret env then
68 ... | false = interpret env else
69 interpret env (While x comm) with x env
70 ... | true = interpret (interpret env comm) (While x comm)
71 ... | false = env
72
73 test1 : Env
74 test1 = interpret ( record { vari = 0 ; varn = 0 } ) program
75
76
77 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true
78 empty-case _ = refl
79
80 implies : Bool → Bool → Bool
81 implies false _ = true
82 implies true true = true
83 implies true false = false
84
85 Axiom : Cond -> PrimComm -> Cond -> Set
86 Axiom pre comm post = ∀ (env : Env) → implies (pre env) ( post (comm env)) ≡ true
87
88 Tautology : Cond -> Cond -> Set
89 Tautology pre post = ∀ (env : Env) → implies (pre env) (post env) ≡ true
90
91 _/\_ : Cond -> Cond -> Cond
92 x /\ y = λ env → x env ∧ y env
93
94 neg : Cond -> Cond
95 neg x = λ env → not ( x env )
96
97 data HTProof : Cond -> Comm -> Cond -> Set where
98 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
99 (pr : Axiom bPre pcm bPost) ->
100 HTProof bPre (PComm pcm) bPost
101 SkipRule : (b : Cond) -> HTProof b Skip b
102 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
103 HTProof bPre Abort bPost
104 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
105 {bPost' : Cond} -> {bPost : Cond} ->
106 Tautology bPre bPre' ->
107 HTProof bPre' cm bPost' ->
108 Tautology bPost' bPost ->
109 HTProof bPre cm bPost
110 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
111 {cm2 : Comm} -> {bPost : Cond} ->
112 HTProof bPre cm1 bMid ->
113 HTProof bMid cm2 bPost ->
114 HTProof bPre (Seq cm1 cm2) bPost
115 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
116 {bPre : Cond} -> {bPost : Cond} ->
117 {b : Cond} ->
118 HTProof (bPre /\ b) cmThen bPost ->
119 HTProof (bPre /\ neg b) cmElse bPost ->
120 HTProof bPre (If b cmThen cmElse) bPost
121 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
122 HTProof (bInv /\ b) cm bInv ->
123 HTProof bInv (While b cm) (bInv /\ neg b)
124
125 initCond : Cond
126 initCond env = true
127
128 stmt1Cond : Cond
129 stmt1Cond env = Equal (varn env) 10
130
131 stmt2Cond : Cond
132 stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)
133
134 whileInv : Cond
135 whileInv env = Equal ((varn env) + (vari env)) 10
136
137 whileInv' : Cond
138 whileInv' env = Equal ((varn env) + (vari env)) 11
139
140 termCond : Cond
141 termCond env = Equal (vari env) 10
142
143 eqlemma : { x y : ℕ } → Equal x y ≡ true → x ≡ y
144 eqlemma {x} {y} eq with x ≟ y
145 eqlemma {x} {y} refl | yes refl = refl
146 eqlemma {x} {y} () | no ¬p
147
148 proofs : HTProof initCond simple stmt2Cond
149 proofs =
150 SeqRule {initCond} ( PrimRule empty-case )
151 $ PrimRule {stmt1Cond} {_} {stmt2Cond} lemma
152 where
153 lemma : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
154 lemma env with stmt1Cond env
155 lemma env | false = refl
156 lemma env | true = refl
157
158
159 proof1 : HTProof initCond program termCond
160 proof1 =
161 SeqRule {λ e → true} ( PrimRule empty-case )
162 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 )
163 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 (
164 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
165 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt (varn e) zero } lemma3)
166 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
167 where
168 lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
169 lemma1 env with stmt1Cond env
170 lemma1 env | false = refl
171 lemma1 env | true = refl
172 lemma2 : Tautology stmt2Cond whileInv
173 lemma2 env with stmt2Cond env | Equal (varn env + vari env) 10
174 lemma2 env | false | false = refl
175 lemma2 env | false | true = refl
176 lemma2 env | true | true = refl
177 lemma2 env | true | false = {!!}
178 lemma3 : Axiom (whileInv /\ (λ env → lt (varn env) zero)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
179 lemma3 = {!!}
180 lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
181 lemma4 = {!!}
182 lemma5 : Tautology (whileInv /\ neg (λ z → lt (varn z) zero)) termCond
183 lemma5 = {!!}
184
185