Mercurial > hg > Members > ryokka > HoareLogic
changeset 70:fdd31b6808db
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 Dec 2019 18:20:42 +0900 |
| parents | 5b17a3601037 |
| children | 57d5a3884898 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 11 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Mon Dec 23 16:36:06 2019 +0900 +++ b/whileTestGears.agda Mon Dec 23 18:20:42 2019 +0900 @@ -203,13 +203,18 @@ whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!} whileLoopPSem env s next exit | tri< a ¬b ¬c = {!!} +loopPP : (input : Envc ) → Envc +loopPP input with <-cmp 0 (varn input ) +loopPP input | tri≈ ¬a b ¬c = input +loopPP input | tri< a ¬b ¬c = {!!} -- loopPP (whileLoopP ? +-- = whileLoopP input (λ next → loopPP next ) (λ output → output ) + whileLoopPSemSound : (input output : Envc ) → whileTestStateP s2 input - → output ≡ whileLoopP input (λ e → whileLoopP e ? (λ e → e ) ) (λ e → e) + → output ≡ loopPP input → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) -whileLoopPSemSound = {!!} - - +whileLoopPSemSound input output pre refl with <-cmp 0 (varn input ) +... | ttt = {!!} -- induction にする {-# TERMINATING #-} @@ -219,8 +224,8 @@ -- wP を Env のRel にする Env → Env → Set にしちゃう whileTestPCallwP : (c : ℕ ) → Set whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where - conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env - conv e record { pi1 = refl ; pi2 = refl } = +zero + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero conv1 : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env