Mercurial > hg > Members > ryokka > HoareLogic
changeset 69:5b17a3601037
try loop
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 Dec 2019 16:36:06 +0900 |
| parents | def072b6c016 |
| children | fdd31b6808db |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 17 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Mon Dec 23 15:57:23 2019 +0900 +++ b/whileTestGears.agda Mon Dec 23 16:36:06 2019 +0900 @@ -190,12 +190,25 @@ GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t) → t ) → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1))) - → e1 ≡ f e0 (λ e → e ) → f e0 (λ e1 → pre e0 implies post e1) -GearsUnitSound e0 e1 f fsem refl = fsem e0 +GearsUnitSound e0 e1 f fsem = fsem e0 + +whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) +whileTestPSemSound c output refl = whileTestPSem c -whileTestPSemSound : (c : ℕ ) (input output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) -whileTestPSemSound c input output refl = whileTestPSem c +whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input + → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) + → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t +whileLoopPSem env s next exit with <-cmp 0 (varn env) +whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!} +whileLoopPSem env s next exit | tri< a ¬b ¬c = {!!} + +whileLoopPSemSound : (input output : Envc ) + → whileTestStateP s2 input + → output ≡ whileLoopP input (λ e → whileLoopP e ? (λ e → e ) ) (λ e → e) + → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) +whileLoopPSemSound = {!!} + -- induction にする