|
3
|
1 -- Nomal CodeGear
|
|
|
2 whileLoop' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc)
|
|
|
3 → (n ≡ varn env)
|
|
|
4 → (next : Envc → t)
|
|
|
5 → (exit : Envc → t) → 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} → (n : ℕ) → (env : Envc )
|
|
|
11 → (n ≡ varn env) → (pre : varn env + vari env ≡ c10 env)
|
|
|
12 → (next : (env : Envc ) → (pred n ≡ varn env) → (post : varn env + vari env ≡ c10 env) → t)
|
|
|
13 → (exit : (env : Envc ) → (fin : vari env ≡ c10 env) → t) → 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))
|
