Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/agda-hoare-write.agda.replaced @ 0:c59202657321
init
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Nov 2021 06:55:58 +0900 |
| parents | |
| children | 339fb67b4375 |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:c59202657321 |
|---|---|
| 1 -- Nomal CodeGear | |
| 2 whileLoop' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) | |
| 3 @$\rightarrow$@ (n @$\equiv$@ varn env) | |
| 4 @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) | |
| 5 @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 6 whileLoop' zero env refl _ exit = exit env | |
| 7 whileLoop' (suc n) env refl next _ = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) | |
| 8 | |
| 9 -- Hoare Logic base CodeGear | |
| 10 whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) | |
| 11 @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (pre : varn env + vari env @$\equiv$@ c10 env) | |
| 12 @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ (post : varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ t) | |
| 13 @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ (fin : vari env @$\equiv$@ c10 env) @$\rightarrow$@ t) @$\rightarrow$@ t | |
| 14 whileLoopPwP' zero env refl refl next exit = exit env refl | |
| 15 whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) |