Mercurial > hg > Members > ryokka > HoareLogic
changeset 82:33a6fd61c3e6
writing Soundness conect
| author | ryokka |
|---|---|
| date | Thu, 02 Jan 2020 20:22:24 +0900 |
| parents | 0122f980427c |
| children | cf5e6afbeb7c |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 27 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Thu Jan 02 15:33:49 2020 +0900 +++ b/whileTestGears.agda Thu Jan 02 20:22:24 2020 +0900 @@ -18,7 +18,7 @@ field varn : ℕ vari : ℕ -open Env +open Env whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t whileTest c10 next = next (record {varn = c10 ; vari = 0 } ) @@ -30,7 +30,7 @@ whileLoop env next | true = whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next -test1 : Env +test1 : Env test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) @@ -42,7 +42,7 @@ 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 : Env env = record {vari = 0 ; varn = c10 } proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition proof2 = record {pi1 = refl ; pi2 = refl} @@ -54,7 +54,7 @@ {-# 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 +whileLoop' env proof next | no p = next env whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1} @@ -65,13 +65,13 @@ proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in begin - n' + (vari env + 1) + n' + (vari env + 1) ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ - n' + (1 + vari env ) + n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ - (n' + 1) + vari env + (n' + 1) + vari env ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ - (suc n' ) + vari env + (suc n' ) + vari env ≡⟨⟩ varn env + vari env ≡⟨ proof ⟩ @@ -97,7 +97,7 @@ -- all proofs are connected proofGears : {c10 : ℕ } → Set -proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -- but we cannot prove the soundness of the last condition -- @@ -147,10 +147,10 @@ s2 : whileTestState sf : whileTestState -whileTestStateP : whileTestState → Envc → Set -whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) -whileTestStateP s2 env = (varn env + vari env ≡ c10 env) -whileTestStateP sf env = (vari env ≡ c10 env) +whileTestStateP : whileTestState → Envc → Set +whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) +whileTestStateP s2 env = (varn env + vari env ≡ c10 env) +whileTestStateP sf env = (vari env ≡ c10 env) whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where @@ -192,7 +192,7 @@ loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit -- all codtions are correctly connected and required condtion is proved in the continuation --- use required condition as t in (env → t) → t +-- use required condition as t in (env → t) → t whileTestPCallwP : (c : ℕ ) → Set whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env @@ -224,17 +224,23 @@ whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) whileTestPSemSound c output refl = whileTestPSem c + +whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input) +whileConvPSemSound input = proof λ x → (conv input x) where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc loopPP zero input refl = input loopPP (suc n) input refl = - loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl + loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t whileLoopPSem env s next exit with varn env | s ... | zero | _ = exit env (proof (λ z → z)) -... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) @@ -244,7 +250,7 @@ lem n env = +-suc (n) (vari env) loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) - loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = whileLoopPSem current refl (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) @@ -256,3 +262,7 @@ → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre + + +whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ → whileTestStateP sf output +whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top = implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileTestP c (λ e → e)) refl) top))