Mercurial > hg > Members > ryokka > HoareLogic
annotate whileTestPrimProof.agda @ 98:2d2b0b06945b default tip
simplfied version
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 Apr 2023 17:00:53 +0900 |
| parents | a7263ecf8671 |
| children |
| rev | line source |
|---|---|
| 23 | 1 module whileTestPrimProof where |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Function |
| 93 | 4 open import Data.Nat renaming ( _∸_ to _-_) |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Bool hiding ( _≟_ ) |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Level renaming ( suc to succ ; zero to Zero ) |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 4 | 8 open import Relation.Binary.PropositionalEquality |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
| 21 | 10 open import utilities hiding ( _/\_ ) |
| 23 | 11 open import whileTestPrim |
|
22
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
12 |
| 24 | 13 open import Hoare PrimComm Cond Axiom Tautology _and_ neg |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
| 23 | 15 open Env |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 initCond : Cond |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 initCond env = true |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
| 14 | 20 stmt1Cond : {c10 : ℕ} → Cond |
| 21 stmt1Cond {c10} env = Equal (varn env) c10 | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
23 init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
24 init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl ) |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
25 |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
26 init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10}) |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
27 init-type {c10} env = init-case env |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
28 |
| 14 | 29 stmt2Cond : {c10 : ℕ} → Cond |
| 30 stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
32 lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
33 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
34 begin |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
35 (Equal (varn env) c10 ) ∧ true |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
36 ≡⟨ ∧true ⟩ |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
37 Equal (varn env) c10 |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
38 ≡⟨ cond ⟩ |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
39 true |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
40 ∎ ) |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
41 |
| 23 | 42 -- simple : ℕ → Comm |
| 43 -- simple c10 = | |
| 44 -- Seq ( PComm (λ env → record env {varn = c10})) | |
| 45 -- $ PComm (λ env → record env {vari = 0}) | |
| 46 | |
| 14 | 47 proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10}) |
| 48 proofs c10 = | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
49 SeqRule {initCond} ( PrimRule (init-case {c10} )) |
|
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
50 $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10}) |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 |
| 8 | 52 open import Data.Empty |
| 53 | |
| 54 open import Data.Nat.Properties | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 |
| 23 | 56 whileInv : {c10 : ℕ} → Cond |
| 57 whileInv {c10} env = Equal ((varn env) + (vari env)) c10 | |
| 58 | |
| 59 whileInv' : {c10 : ℕ} → Cond | |
| 60 whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env) | |
| 61 | |
| 62 termCond : {c10 : ℕ} → Cond | |
| 63 termCond {c10} env = Equal (vari env) c10 | |
| 64 | |
| 65 | |
| 66 -- program : ℕ → Comm | |
| 67 -- program c10 = | |
| 68 -- Seq ( PComm (λ env → record env {varn = c10})) | |
| 69 -- $ Seq ( PComm (λ env → record env {vari = 0})) | |
| 70 -- $ While (λ env → lt zero (varn env ) ) | |
| 71 -- (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) | |
| 72 -- $ PComm (λ env → record env {varn = ((varn env) - 1)} )) | |
| 73 | |
| 61 | 74 |
| 14 | 75 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) |
| 76 proof1 c10 = | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
77 SeqRule {λ e → true} ( PrimRule (init-case {c10} )) |
| 14 | 78 $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) |
| 79 $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( | |
| 80 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} | |
| 7 | 81 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) |
| 82 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 where |
| 14 | 84 lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 |
| 10 | 85 lemma21 eq = Equal→≡ (∧-pi1 eq) |
| 14 | 86 lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 |
| 10 | 87 lemma22 eq = Equal→≡ (∧-pi2 eq) |
| 14 | 88 lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 |
| 89 lemma23 {env} {c10} eq = let open ≡-Reasoning in | |
| 8 | 90 begin |
| 91 varn env + vari env | |
| 92 ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ | |
| 14 | 93 c10 + vari env |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
94 ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ |
| 14 | 95 c10 + 0 |
| 96 ≡⟨ +-sym {c10} {0} ⟩ | |
| 97 0 + c10 | |
| 98 ≡⟨⟩ | |
| 99 c10 | |
| 8 | 100 ∎ |
| 14 | 101 lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv |
| 102 lemma2 {c10} env = bool-case (stmt2Cond env) ( | |
| 8 | 103 λ eq → let open ≡-Reasoning in |
| 104 begin | |
| 10 | 105 (stmt2Cond env) ⇒ (whileInv env) |
| 8 | 106 ≡⟨⟩ |
| 14 | 107 (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) |
| 108 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ | |
| 109 (stmt2Cond env) ⇒ (Equal c10 c10) | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
110 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ |
| 14 | 111 (stmt2Cond {c10} env) ⇒ true |
| 10 | 112 ≡⟨ ⇒t ⟩ |
| 8 | 113 true |
| 114 ∎ | |
| 115 ) ( | |
| 116 λ ne → let open ≡-Reasoning in | |
| 117 begin | |
| 10 | 118 (stmt2Cond env) ⇒ (whileInv env) |
| 119 ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ | |
| 14 | 120 false ⇒ (whileInv {c10} env) |
| 121 ≡⟨ f⇒ {whileInv {c10} env} ⟩ | |
| 8 | 122 true |
| 123 ∎ | |
| 124 ) | |
| 7 | 125 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' |
| 10 | 126 lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in |
| 8 | 127 begin |
| 128 whileInv' (record { varn = varn env ; vari = vari env + 1 }) | |
| 129 ≡⟨⟩ | |
| 14 | 130 Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) |
| 131 ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ | |
| 132 Equal (varn env + (vari env + 1)) (suc c10) ∧ true | |
| 10 | 133 ≡⟨ ∧true ⟩ |
| 14 | 134 Equal (varn env + (vari env + 1)) (suc c10) |
| 135 ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ | |
| 136 Equal ((varn env + vari env) + 1) (suc c10) | |
| 137 ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ | |
| 138 Equal (suc (varn env + vari env)) (suc c10) | |
| 10 | 139 ≡⟨ sym Equal+1 ⟩ |
| 14 | 140 Equal ((varn env + vari env) ) c10 |
| 10 | 141 ≡⟨ ∧-pi1 cond ⟩ |
| 8 | 142 true |
| 143 ∎ ) | |
| 14 | 144 lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true |
| 145 lemma41 env {c10} c1 c2 = let open ≡-Reasoning in | |
| 10 | 146 begin |
| 14 | 147 Equal ((varn env - 1) + vari env) c10 |
| 148 ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ | |
| 149 Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 | |
| 10 | 150 ≡⟨⟩ |
| 14 | 151 Equal ((predℕ {varn env} c2 ) + vari env) c10 |
| 10 | 152 ≡⟨ Equal+1 ⟩ |
| 14 | 153 Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) |
| 154 ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ | |
| 155 Equal (varn env + vari env) (suc c10) | |
| 156 ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ | |
| 157 Equal (suc c10) (suc c10) | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
158 ≡⟨ ≡→Equal refl ⟩ |
| 10 | 159 true |
| 160 ∎ | |
| 14 | 161 lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv |
| 162 lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in | |
| 10 | 163 begin |
| 164 whileInv (record { varn = varn env - 1 ; vari = vari env }) | |
| 165 ≡⟨⟩ | |
| 14 | 166 Equal ((varn env - 1) + vari env) c10 |
| 10 | 167 ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ |
| 168 true | |
| 169 ∎ | |
| 170 ) | |
| 171 lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero | |
| 17 | 172 lemma51 z cond with varn z |
| 173 lemma51 z refl | zero = refl | |
| 174 lemma51 z () | suc x | |
| 14 | 175 lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond |
| 176 lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in | |
| 10 | 177 begin |
| 178 termCond env | |
| 179 ≡⟨⟩ | |
| 14 | 180 Equal (vari env) c10 |
| 10 | 181 ≡⟨⟩ |
| 14 | 182 Equal (zero + vari env) c10 |
| 183 ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ | |
| 184 Equal (varn env + vari env) c10 | |
| 10 | 185 ≡⟨ ∧-pi1 cond ⟩ |
| 186 true | |
| 187 ∎ | |
| 188 ) | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
189 |
| 21 | 190 --- necessary definitions for Hoare.agda ( Soundness ) |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
191 |
| 21 | 192 State : Set |
| 193 State = Env | |
| 10 | 194 |
| 21 | 195 open import RelOp |
| 196 module RelOpState = RelOp State | |
| 197 | |
| 198 open import Data.Product | |
| 199 open import Relation.Binary | |
| 200 | |
| 201 NotP : {S : Set} -> Pred S -> Pred S | |
| 202 NotP X s = ¬ X s | |
| 203 | |
| 204 _/\_ : Cond -> Cond -> Cond | |
| 205 b1 /\ b2 = b1 and b2 | |
| 206 | |
| 207 _\/_ : Cond -> Cond -> Cond | |
| 208 b1 \/ b2 = neg (neg b1 /\ neg b2) | |
| 209 | |
| 210 SemCond : Cond -> State -> Set | |
| 211 SemCond c p = c p ≡ true | |
| 212 | |
| 213 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> | |
| 214 (s : State) -> SemCond b1 s -> SemCond b2 s | |
| 215 tautValid b1 b2 taut s cond with b1 s | b2 s | taut s | |
| 216 tautValid b1 b2 taut s () | false | false | refl | |
| 217 tautValid b1 b2 taut s _ | false | true | refl = refl | |
| 218 tautValid b1 b2 taut s _ | true | false | () | |
| 219 tautValid b1 b2 taut s _ | true | true | refl = refl | |
| 220 | |
| 221 respNeg : (b : Cond) -> (s : State) -> | |
| 222 Iff (SemCond (neg b) s) (¬ SemCond b s) | |
| 223 respNeg b s = ( left , right ) where | |
| 224 left : not (b s) ≡ true → (b s) ≡ true → ⊥ | |
| 225 left ne with b s | |
| 226 left refl | false = λ () | |
| 227 left () | true | |
| 228 right : ((b s) ≡ true → ⊥) → not (b s) ≡ true | |
| 229 right ne with b s | |
| 230 right ne | false = refl | |
| 231 right ne | true = ⊥-elim ( ne refl ) | |
| 232 | |
| 233 respAnd : (b1 b2 : Cond) -> (s : State) -> | |
| 234 Iff (SemCond (b1 /\ b2) s) | |
| 235 ((SemCond b1 s) × (SemCond b2 s)) | |
| 236 respAnd b1 b2 s = ( left , right ) where | |
| 237 left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true) | |
| 238 left and with b1 s | b2 s | |
| 239 left () | false | false | |
| 240 left () | false | true | |
| 241 left () | true | false | |
| 242 left refl | true | true = ( refl , refl ) | |
| 243 right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true | |
| 244 right ( x1 , x2 ) with b1 s | b2 s | |
| 245 right (() , ()) | false | false | |
| 246 right (() , _) | false | true | |
| 247 right (_ , ()) | true | false | |
| 248 right (refl , refl) | true | true = refl | |
| 249 | |
| 250 PrimSemComm : ∀ {l} -> PrimComm -> Rel State l | |
| 251 PrimSemComm prim s1 s2 = Id State (prim s1) s2 | |
| 252 | |
| 66 | 253 |
| 254 | |
| 21 | 255 axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> |
| 256 (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> | |
| 257 SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2 | |
| 258 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1 | |
| 259 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl | |
| 260 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl | |
| 261 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () | |
| 262 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl | |
| 263 | |
| 24 | 264 open import HoareSoundness |
|
22
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
265 Cond |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
266 PrimComm |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
267 neg |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
268 _and_ |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
269 Tautology |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
270 State |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
271 SemCond |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
272 tautValid |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
273 respNeg |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
274 respAnd |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
275 PrimSemComm |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
276 Axiom |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
277 axiomValid |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
278 |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
279 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
280 HTProof bPre cm bPost -> Satisfies bPre cm bPost |
|
e88ad1d70faf
separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
281 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht |
| 61 | 282 |
| 283 | |
| 284 proofOfProgram : (c10 : ℕ) → (input output : Env ) | |
| 285 → initCond input ≡ true | |
| 286 → (SemComm (program c10) input output) | |
| 287 → termCond {c10} output ≡ true | |
| 288 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem |