Mercurial > hg > Papers > 2020 > soto-midterm
view src/agda-hoare-write.agda @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line source
-- Nomal CodeGear whileLoop' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc) → (n ≡ varn env) → (next : Envc → t) → (exit : Envc → t) → t whileLoop' zero env refl _ exit = exit env whileLoop' (suc n) env refl next _ = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) -- Hoare Logic base CodeGear whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → (pre : varn env + vari env ≡ c10 env) → (next : (env : Envc ) → (pred n ≡ varn env) → (post : varn env + vari env ≡ c10 env) → t) → (exit : (env : Envc ) → (fin : vari env ≡ c10 env) → t) → t whileLoopPwP' zero env refl refl next exit = exit env refl whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))