Mercurial > hg > Members > ryokka > HoareLogic

comparison Hoare.agda @ 24:e668962ac31a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rename modules
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Dec 2018 08:45:06 +0900
parents HoareData.agda@e88ad1d70faf
children
comparison
equal deleted inserted replaced
23:3968822b9693 24:e668962ac31a
1 {-# OPTIONS --universe-polymorphism #-} 1 module Hoare
2 (PrimComm : Set)
3 (Cond : Set)
4 (Axiom : Cond -> PrimComm -> Cond -> Set)
5 (Tautology : Cond -> Cond -> Set)
6 (_and_ : Cond -> Cond -> Cond)
7 (neg : Cond -> Cond )
8 where
2 9
3 open import Level 10 data Comm : Set where
4 open import Data.Nat 11 Skip : Comm
5 open import Data.Product 12 Abort : Comm
6 open import Data.Bool 13 PComm : PrimComm -> Comm
7 open import Data.Empty 14 Seq : Comm -> Comm -> Comm
8 open import Data.Sum 15 If : Cond -> Comm -> Comm -> Comm
9 open import Relation.Binary 16 While : Cond -> Comm -> Comm
10 open import Relation.Nullary
11 open import Relation.Binary.Core
12 open import Relation.Binary.PropositionalEquality
13 open import RelOp
14 open import utilities
15 17
16 module Hoare
17 (Cond : Set)
18 (PrimComm : Set)
19 (neg : Cond -> Cond)
20 (_/\_ : Cond -> Cond -> Cond)
21 (Tautology : Cond -> Cond -> Set)
22 (State : Set)
23 (SemCond : Cond -> State -> Set)
24 (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->
25 (s : State) -> SemCond b1 s -> SemCond b2 s)
26 (respNeg : (b : Cond) -> (s : State) ->
27 Iff (SemCond (neg b) s) (¬ SemCond b s))
28 (respAnd : (b1 b2 : Cond) -> (s : State) ->
29 Iff (SemCond (b1 /\ b2) s)
30 ((SemCond b1 s) × (SemCond b2 s)))
31 (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l)
32 (Axiom : Cond -> PrimComm -> Cond -> Set)
33 (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
34 (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
35 SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where
36 18
37 open import HoareData PrimComm Cond Axiom Tautology _/\_ neg 19 {-
20 prPre pr prPost
21 ------------- ------------------ ----------------
22 bPre => bPre' {bPre'} c {bPost'} bPost' => bPost
23 Weakening : ----------------------------------------------------
24 {bPre} c {bPost}
38 25
39 open import RelOp 26 Assign: ----------------------------
40 module RelOpState = RelOp State 27 {bPost[v<-e]} v:=e {bPost}
41 28
42 NotP : {S : Set} -> Pred S -> Pred S 29 pr1 pr2
43 NotP X s = ¬ X s 30 ----------------- ------------------
31 {bPre} cm1 {bMid} {bMid} cm2 {bPost}
32 Seq: ---------------------------------------
33 {bPre} cm1 ; cm2 {bPost}
44 34
45 _\/_ : Cond -> Cond -> Cond 35 pr1 pr2
46 b1 \/ b2 = neg (neg b1 /\ neg b2) 36 ----------------------- ---------------------------
37 {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost}
38 If: ------------------------------------------------------
39 {bPre} If c then cm1 else cm2 fi {bPost}
47 40
48 _==>_ : Cond -> Cond -> Cond 41 pr
49 b1 ==> b2 = neg (b1 \/ b2) 42 -------------------
43 {inv /\ c} cm {inv}
44 While: ---------------------------------------
45 {inv} while c do cm od {inv /\ neg c}
46 -}
50 47
51 when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) ->
52 X ⊎ Y -> Z
53 when f g (inj₁ x) = f x
54 when f g (inj₂ y) = g y
55 48
56 -- semantics of commands 49 data HTProof : Cond -> Comm -> Cond -> Set where
57 SemComm : Comm -> Rel State (Level.zero) 50 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
58 SemComm Skip = RelOpState.deltaGlob 51 (pr : Axiom bPre pcm bPost) ->
59 SemComm Abort = RelOpState.emptyRel 52 HTProof bPre (PComm pcm) bPost
60 SemComm (PComm pc) = PrimSemComm pc 53 SkipRule : (b : Cond) -> HTProof b Skip b
61 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) 54 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
62 SemComm (If b c1 c2) 55 HTProof bPre Abort bPost
63 = RelOpState.union 56 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
64 (RelOpState.comp (RelOpState.delta (SemCond b)) 57 {bPost' : Cond} -> {bPost : Cond} ->
65 (SemComm c1)) 58 Tautology bPre bPre' ->
66 (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) 59 HTProof bPre' cm bPost' ->
67 (SemComm c2)) 60 Tautology bPost' bPost ->
68 SemComm (While b c) 61 HTProof bPre cm bPost
69 = RelOpState.unionInf 62 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
70 (λ (n : ℕ) -> 63 {cm2 : Comm} -> {bPost : Cond} ->
71 RelOpState.comp (RelOpState.repeat 64 HTProof bPre cm1 bMid ->
72 n 65 HTProof bMid cm2 bPost ->
73 (RelOpState.comp 66 HTProof bPre (Seq cm1 cm2) bPost
74 (RelOpState.delta (SemCond b)) 67 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
75 (SemComm c))) 68 {bPre : Cond} -> {bPost : Cond} ->
76 (RelOpState.delta (NotP (SemCond b)))) 69 {b : Cond} ->
70 HTProof (bPre and b) cmThen bPost ->
71 HTProof (bPre and neg b) cmElse bPost ->
72 HTProof bPre (If b cmThen cmElse) bPost
73 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
74 HTProof (bInv and b) cm bInv ->
75 HTProof bInv (While b cm) (bInv and neg b)
77 76
78 Satisfies : Cond -> Comm -> Cond -> Set
79 Satisfies bPre cm bPost
80 = (s1 : State) -> (s2 : State) ->
81 SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
82
83 Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
84 HTProof bPre cm bPost -> Satisfies bPre cm bPost
85 Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
86 = axiomValid bPre cm bPost pr s1 s2 q1 q2
87 Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
88 = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
89 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
90 Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
91 s1 s2 q1 q2
92 = let hyp : Satisfies bPre' cm bPost'
93 hyp = Soundness pr
94 r1 : SemCond bPre' s1
95 r1 = tautValid bPre bPre' tautPre s1 q1
96 r2 : SemCond bPost' s2
97 r2 = hyp s1 s2 r1 q2
98 in tautValid bPost' bPost tautPost s2 r2
99 Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
100 s1 s2 q1 q2
101 = let hyp1 : Satisfies bPre cm1 bMid
102 hyp1 = Soundness pr1
103 hyp2 : Satisfies bMid cm2 bPost
104 hyp2 = Soundness pr2
105 sMid : State
106 sMid = proj₁ q2
107 r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2
108 r1 = proj₂ q2
109 r2 : SemComm cm1 s1 sMid
110 r2 = proj₁ r1
111 r3 : SemComm cm2 sMid s2
112 r3 = proj₂ r1
113 r4 : SemCond bMid sMid
114 r4 = hyp1 s1 sMid q1 r2
115 in hyp2 sMid s2 r4 r3
116 Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
117 s1 s2 q1 q2
118 = let hypThen : Satisfies (bPre /\ b) cmThen bPost
119 hypThen = Soundness pThen
120 hypElse : Satisfies (bPre /\ neg b) cmElse bPost
121 hypElse = Soundness pElse
122 rThen : RelOpState.comp
123 (RelOpState.delta (SemCond b))
124 (SemComm cmThen) s1 s2 ->
125 SemCond bPost s2
126 rThen = λ h ->
127 let t1 : SemCond b s1 × SemComm cmThen s1 s2
128 t1 = (proj₂ (RelOpState.deltaRestPre
129 (SemCond b)
130 (SemComm cmThen) s1 s2)) h
131 t2 : SemCond (bPre /\ b) s1
132 t2 = (proj₂ (respAnd bPre b s1))
133 (q1 , proj₁ t1)
134 in hypThen s1 s2 t2 (proj₂ t1)
135 rElse : RelOpState.comp
136 (RelOpState.delta (NotP (SemCond b)))
137 (SemComm cmElse) s1 s2 ->
138 SemCond bPost s2
139 rElse = λ h ->
140 let t10 : (NotP (SemCond b) s1) ×
141 (SemComm cmElse s1 s2)
142 t10 = proj₂ (RelOpState.deltaRestPre
143 (NotP (SemCond b)) (SemComm cmElse) s1 s2)
144 h
145 t6 : SemCond (neg b) s1
146 t6 = proj₂ (respNeg b s1) (proj₁ t10)
147 t7 : SemComm cmElse s1 s2
148 t7 = proj₂ t10
149 t8 : SemCond (bPre /\ neg b) s1
150 t8 = proj₂ (respAnd bPre (neg b) s1)
151 (q1 , t6)
152 in hypElse s1 s2 t8 t7
153 in when rThen rElse q2
154 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
155 = proj₂ (respAnd bInv (neg b) s2) t20
156 where
157 hyp : Satisfies (bInv /\ b) cm' bInv
158 hyp = Soundness pr
159 n : ℕ
160 n = proj₁ q2
161 Rel1 : ℕ -> Rel State (Level.zero)
162 Rel1 = λ m ->
163 RelOpState.repeat
164 m
165 (RelOpState.comp (RelOpState.delta (SemCond b))
166 (SemComm cm'))
167 t1 : RelOpState.comp
168 (Rel1 n)
169 (RelOpState.delta (NotP (SemCond b))) s1 s2
170 t1 = proj₂ q2
171 t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
172 t15 = proj₂ (RelOpState.deltaRestPost
173 (NotP (SemCond b)) (Rel1 n) s1 s2)
174 t1
175 t16 : Rel1 n s1 s2
176 t16 = proj₁ t15
177 t17 : NotP (SemCond b) s2
178 t17 = proj₂ t15
179 lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 ->
180 SemCond bInv ss2
181 lem1 ℕ.zero ss2 h
182 = substId1 State (proj₂ h) (SemCond bInv) q1
183 lem1 (ℕ.suc n) ss2 h
184 = let hyp2 : (z : State) -> Rel1 n s1 z ->
185 SemCond bInv z
186 hyp2 = lem1 n
187 s20 : State
188 s20 = proj₁ h
189 t21 : Rel1 n s1 s20
190 t21 = proj₁ (proj₂ h)
191 t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
192 t22 = proj₂ (RelOpState.deltaRestPre
193 (SemCond b) (SemComm cm') s20 ss2)
194 (proj₂ (proj₂ h))
195 t23 : SemCond (bInv /\ b) s20
196 t23 = proj₂ (respAnd bInv b s20)
197 (hyp2 s20 t21 , proj₁ t22)
198 in hyp s20 ss2 t23 (proj₂ t22)
199 t20 : SemCond bInv s2 × SemCond (neg b) s2
200 t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17