Mercurial > hg > Members > ryokka > HoareLogic
changeset 16:23cce7437918
add comment
| author | ryokka |
|---|---|
| date | Sun, 16 Dec 2018 19:31:36 +0900 |
| parents | 8d546766a9a8 |
| children | b95a3cf9727c cc6db47d6882 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 4 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Sun Dec 16 11:20:53 2018 +0900 +++ b/whileTestGears.agda Sun Dec 16 19:31:36 2018 +0900 @@ -33,19 +33,20 @@ proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) proof1 = refl +-- ↓PostCondition whileTest' : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) -> ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t whileTest' {_} {_} {c10} next = next env proof2 where env : Env env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition proof2 = record {pi1 = refl ; pi2 = refl} open import Data.Empty open import Data.Nat.Properties -{-# TERMINATING #-} +{-# TERMINATING #-} -- ↓PreCondition(Invaliant) whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) -> (Code : Env -> t) -> t whileLoop' env proof next with ( suc zero ≤? (varn env) ) whileLoop' env proof next | no p = next env @@ -72,7 +73,7 @@ c10 ∎ - +-- Condition to Invaliant conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t conversion1 env {c10} p1 next = next env proof4