Mercurial > hg > Members > ryokka > HoareLogic
changeset 31:600b4e914071
fix loop
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 10 Dec 2019 09:19:14 +0900 |
| parents | dd66b94bf365 |
| children | bf7c7bd69e35 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 14 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Tue Dec 10 08:57:11 2019 +0900 +++ b/whileTestGears.agda Tue Dec 10 09:19:14 2019 +0900 @@ -147,38 +147,32 @@ {-# TERMINATING #-} whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t -whileLoopProof cxt next exit = next record cxt { whileDG = out ; whileCond = postCond } where - out : Env - out = whileLoopStep (whileDG cxt) ( λ e → e ) {!!} - postCond : whileTestState (c10 cxt) - postCond with whileCond cxt - ... | state2 e inv = state2 out {!!} where - proof3 : {!!} - proof3 = {!!} - ... | _ = error +whileLoopProof cxt next exit = whileLoopStep (whileDG cxt) + ( λ env → next record cxt { whileDG = env ; whileCond = nextCond env } ) + ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } ) where + nextCond : Env → whileTestState (c10 cxt) + nextCond nenv with whileCond cxt + ... | state2 e inv = state2 (whileDG cxt) {!!} + ... | _ = error + exitCond : Env → whileTestState (c10 cxt) + exitCond nenv with whileCond cxt + ... | state2 e inv = finstate (whileDG cxt) {!!} + ... | _ = error whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t whileConvProof cxt next = next record cxt { whileCond = postCond } where postCond : whileTestState (c10 cxt) postCond with whileCond cxt - ... | state1 e inv = state2 (whileDG cxt) {!!} - ... | _ = error - -whileFinConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t -whileFinConvProof cxt next = next record cxt { whileCond = postCond } where - postCond : whileTestState (c10 cxt) - postCond with whileCond cxt - ... | state2 e inv = finstate (whileDG cxt) {!!} + ... | state1 e inv = state2 (whileDG cxt) {!!} ... | _ = error {-# TERMINATING #-} loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t -loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit) exit +loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) $ λ cxt → whileConvProof cxt $ λ cxt → loop cxt - $ λ cxt → whileFinConvProof cxt $ λ cxt → vari (whileDG cxt) ≡ c10 cxt -proofWhileGear cxt = refl +proofWhileGear cxt = {!!}