Mercurial > hg > Papers > 2021 > soto-thesis
view prepaper/src/agda-hoare-write.agda @ 14:a63df15c9afc default tip
DONE
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 15 Feb 2021 23:36:39 +0900 (2021-02-15) |
parents | 3dba680da508 |
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))