Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 31:600b4e914071

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix loop
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 Dec 2019 09:19:14 +0900
parents dd66b94bf365
children bf7c7bd69e35
comparison
equal deleted inserted replaced
30:dd66b94bf365 31:600b4e914071
145 init : whileTestState (c10 cxt) 145 init : whileTestState (c10 cxt)
146 init = state1 out record { pi1 = refl ; pi2 = refl } 146 init = state1 out record { pi1 = refl ; pi2 = refl }
147 147
148 {-# TERMINATING #-} 148 {-# TERMINATING #-}
149 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t 149 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t
150 whileLoopProof cxt next exit = next record cxt { whileDG = out ; whileCond = postCond } where 150 whileLoopProof cxt next exit = whileLoopStep (whileDG cxt)
151 out : Env 151 ( λ env → next record cxt { whileDG = env ; whileCond = nextCond env } )
152 out = whileLoopStep (whileDG cxt) ( λ e → e ) {!!} 152 ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } ) where
153 postCond : whileTestState (c10 cxt) 153 nextCond : Env → whileTestState (c10 cxt)
154 postCond with whileCond cxt 154 nextCond nenv with whileCond cxt
155 ... | state2 e inv = state2 out {!!} where 155 ... | state2 e inv = state2 (whileDG cxt) {!!}
156 proof3 : {!!} 156 ... | _ = error
157 proof3 = {!!} 157 exitCond : Env → whileTestState (c10 cxt)
158 ... | _ = error 158 exitCond nenv with whileCond cxt
159 ... | state2 e inv = finstate (whileDG cxt) {!!}
160 ... | _ = error
159 161
160 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t 162 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
161 whileConvProof cxt next = next record cxt { whileCond = postCond } where 163 whileConvProof cxt next = next record cxt { whileCond = postCond } where
162 postCond : whileTestState (c10 cxt) 164 postCond : whileTestState (c10 cxt)
163 postCond with whileCond cxt 165 postCond with whileCond cxt
164 ... | state1 e inv = state2 (whileDG cxt) {!!} 166 ... | state1 e inv = state2 (whileDG cxt) {!!}
165 ... | _ = error
166
167 whileFinConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
168 whileFinConvProof cxt next = next record cxt { whileCond = postCond } where
169 postCond : whileTestState (c10 cxt)
170 postCond with whileCond cxt
171 ... | state2 e inv = finstate (whileDG cxt) {!!}
172 ... | _ = error 167 ... | _ = error
173 168
174 {-# TERMINATING #-} 169 {-# TERMINATING #-}
175 loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t 170 loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t
176 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit) exit 171 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
177 172
178 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 173 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
179 $ λ cxt → whileConvProof cxt 174 $ λ cxt → whileConvProof cxt
180 $ λ cxt → loop cxt 175 $ λ cxt → loop cxt
181 $ λ cxt → whileFinConvProof cxt
182 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt 176 $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
183 proofWhileGear cxt = refl 177 proofWhileGear cxt = {!!}
184 178