Mercurial > hg > Members > ryokka > HoareLogic

comparison HoareSoundness.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 Hoare.agda@e88ad1d70faf
children 222dd3869ab0
comparison
equal deleted inserted replaced
23:3968822b9693 24:e668962ac31a
1 {-# OPTIONS --universe-polymorphism #-}
2
3 open import Level
4 open import Data.Nat
5 open import Data.Product
6 open import Data.Bool
7 open import Data.Empty
8 open import Data.Sum
9 open import Relation.Binary
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
16 module HoareSoundness
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
37 open import Hoare PrimComm Cond Axiom Tautology _/\_ neg
38
39 open import RelOp
40 module RelOpState = RelOp State
41
42 NotP : {S : Set} -> Pred S -> Pred S
43 NotP X s = ¬ X s
44
45 _\/_ : Cond -> Cond -> Cond
46 b1 \/ b2 = neg (neg b1 /\ neg b2)
47
48 _==>_ : Cond -> Cond -> Cond
49 b1 ==> b2 = neg (b1 \/ b2)
50
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
56 -- semantics of commands
57 SemComm : Comm -> Rel State (Level.zero)
58 SemComm Skip = RelOpState.deltaGlob
59 SemComm Abort = RelOpState.emptyRel
60 SemComm (PComm pc) = PrimSemComm pc
61 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
62 SemComm (If b c1 c2)
63 = RelOpState.union
64 (RelOpState.comp (RelOpState.delta (SemCond b))
65 (SemComm c1))
66 (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
67 (SemComm c2))
68 SemComm (While b c)
69 = RelOpState.unionInf
70 (λ (n : ℕ) ->
71 RelOpState.comp (RelOpState.repeat
72 n
73 (RelOpState.comp
74 (RelOpState.delta (SemCond b))
75 (SemComm c)))
76 (RelOpState.delta (NotP (SemCond b))))
77
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