Mercurial > hg > Members > ryokka > HoareLogic
annotate whileTestPrimProof.agda @ 50:2edb44c5bf52
add s1~3, proofs
| author | ryokka |
|---|---|
| date | Wed, 18 Dec 2019 20:08:58 +0900 |
| parents | e668962ac31a |
| children | 62dcb0ae2c94 |
| 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 |
|
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Data.Nat |
|
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 | |
| 14 | 74 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) |
| 75 proof1 c10 = | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
76 SeqRule {λ e → true} ( PrimRule (init-case {c10} )) |
| 14 | 77 $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) |
| 78 $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( | |
| 79 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} | |
| 7 | 80 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) |
| 81 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 where |
| 14 | 83 lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 |
| 10 | 84 lemma21 eq = Equal→≡ (∧-pi1 eq) |
| 14 | 85 lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 |
| 10 | 86 lemma22 eq = Equal→≡ (∧-pi2 eq) |
| 14 | 87 lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 |
| 88 lemma23 {env} {c10} eq = let open ≡-Reasoning in | |
| 8 | 89 begin |
| 90 varn env + vari env | |
| 91 ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ | |
| 14 | 92 c10 + vari env |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
93 ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ |
| 14 | 94 c10 + 0 |
| 95 ≡⟨ +-sym {c10} {0} ⟩ | |
| 96 0 + c10 | |
| 97 ≡⟨⟩ | |
| 98 c10 | |
| 8 | 99 ∎ |
| 14 | 100 lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv |
| 101 lemma2 {c10} env = bool-case (stmt2Cond env) ( | |
| 8 | 102 λ eq → let open ≡-Reasoning in |
| 103 begin | |
| 10 | 104 (stmt2Cond env) ⇒ (whileInv env) |
| 8 | 105 ≡⟨⟩ |
| 14 | 106 (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) |
| 107 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ | |
| 108 (stmt2Cond env) ⇒ (Equal c10 c10) | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
109 ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ |
| 14 | 110 (stmt2Cond {c10} env) ⇒ true |
| 10 | 111 ≡⟨ ⇒t ⟩ |
| 8 | 112 true |
| 113 ∎ | |
| 114 ) ( | |
| 115 λ ne → let open ≡-Reasoning in | |
| 116 begin | |
| 10 | 117 (stmt2Cond env) ⇒ (whileInv env) |
| 118 ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ | |
| 14 | 119 false ⇒ (whileInv {c10} env) |
| 120 ≡⟨ f⇒ {whileInv {c10} env} ⟩ | |
| 8 | 121 true |
| 122 ∎ | |
| 123 ) | |
| 7 | 124 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' |
| 10 | 125 lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in |
| 8 | 126 begin |
| 127 whileInv' (record { varn = varn env ; vari = vari env + 1 }) | |
| 128 ≡⟨⟩ | |
| 14 | 129 Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) |
| 130 ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ | |
| 131 Equal (varn env + (vari env + 1)) (suc c10) ∧ true | |
| 10 | 132 ≡⟨ ∧true ⟩ |
| 14 | 133 Equal (varn env + (vari env + 1)) (suc c10) |
| 134 ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ | |
| 135 Equal ((varn env + vari env) + 1) (suc c10) | |
| 136 ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ | |
| 137 Equal (suc (varn env + vari env)) (suc c10) | |
| 10 | 138 ≡⟨ sym Equal+1 ⟩ |
| 14 | 139 Equal ((varn env + vari env) ) c10 |
| 10 | 140 ≡⟨ ∧-pi1 cond ⟩ |
| 8 | 141 true |
| 142 ∎ ) | |
| 14 | 143 lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true |
| 144 lemma41 env {c10} c1 c2 = let open ≡-Reasoning in | |
| 10 | 145 begin |
| 14 | 146 Equal ((varn env - 1) + vari env) c10 |
| 147 ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ | |
| 148 Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 | |
| 10 | 149 ≡⟨⟩ |
| 14 | 150 Equal ((predℕ {varn env} c2 ) + vari env) c10 |
| 10 | 151 ≡⟨ Equal+1 ⟩ |
| 14 | 152 Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) |
| 153 ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ | |
| 154 Equal (varn env + vari env) (suc c10) | |
| 155 ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ | |
| 156 Equal (suc c10) (suc c10) | |
|
15
8d546766a9a8
Prim variable version done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
157 ≡⟨ ≡→Equal refl ⟩ |
| 10 | 158 true |
| 159 ∎ | |
| 14 | 160 lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv |
| 161 lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in | |
| 10 | 162 begin |
| 163 whileInv (record { varn = varn env - 1 ; vari = vari env }) | |
| 164 ≡⟨⟩ | |
| 14 | 165 Equal ((varn env - 1) + vari env) c10 |
| 10 | 166 ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ |
| 167 true | |
| 168 ∎ | |
| 169 ) | |
| 170 lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero | |
| 17 | 171 lemma51 z cond with varn z |
| 172 lemma51 z refl | zero = refl | |
| 173 lemma51 z () | suc x | |
| 14 | 174 lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond |
| 175 lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in | |
| 10 | 176 begin |
| 177 termCond env | |
| 178 ≡⟨⟩ | |
| 14 | 179 Equal (vari env) c10 |
| 10 | 180 ≡⟨⟩ |
| 14 | 181 Equal (zero + vari env) c10 |
| 182 ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ | |
| 183 Equal (varn env + vari env) c10 | |
| 10 | 184 ≡⟨ ∧-pi1 cond ⟩ |
| 185 true | |
| 186 ∎ | |
| 187 ) | |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
188 |
| 21 | 189 --- necessary definitions for Hoare.agda ( Soundness ) |
|
3
6be8ee856666
add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
190 |
| 21 | 191 State : Set |
| 192 State = Env | |
| 10 | 193 |
| 21 | 194 open import RelOp |
| 195 module RelOpState = RelOp State | |
| 196 | |
| 197 open import Data.Product | |
| 198 open import Relation.Binary | |
| 199 | |
| 200 NotP : {S : Set} -> Pred S -> Pred S | |
| 201 NotP X s = ¬ X s | |
| 202 | |
| 203 _/\_ : Cond -> Cond -> Cond | |
| 204 b1 /\ b2 = b1 and b2 | |
| 205 | |
| 206 _\/_ : Cond -> Cond -> Cond | |
| 207 b1 \/ b2 = neg (neg b1 /\ neg b2) | |
| 208 | |
| 209 _==>_ : Cond -> Cond -> Cond | |
| 210 b1 ==> b2 = neg (b1 \/ b2) | |
| 211 | |
| 212 SemCond : Cond -> State -> Set | |
| 213 SemCond c p = c p ≡ true | |
| 214 | |
| 215 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> | |
| 216 (s : State) -> SemCond b1 s -> SemCond b2 s | |
| 217 tautValid b1 b2 taut s cond with b1 s | b2 s | taut s | |
| 218 tautValid b1 b2 taut s () | false | false | refl | |
| 219 tautValid b1 b2 taut s _ | false | true | refl = refl | |
| 220 tautValid b1 b2 taut s _ | true | false | () | |
| 221 tautValid b1 b2 taut s _ | true | true | refl = refl | |
| 222 | |
| 223 respNeg : (b : Cond) -> (s : State) -> | |
| 224 Iff (SemCond (neg b) s) (¬ SemCond b s) | |
| 225 respNeg b s = ( left , right ) where | |
| 226 left : not (b s) ≡ true → (b s) ≡ true → ⊥ | |
| 227 left ne with b s | |
| 228 left refl | false = λ () | |
| 229 left () | true | |
| 230 right : ((b s) ≡ true → ⊥) → not (b s) ≡ true | |
| 231 right ne with b s | |
| 232 right ne | false = refl | |
| 233 right ne | true = ⊥-elim ( ne refl ) | |
| 234 | |
| 235 respAnd : (b1 b2 : Cond) -> (s : State) -> | |
| 236 Iff (SemCond (b1 /\ b2) s) | |
| 237 ((SemCond b1 s) × (SemCond b2 s)) | |
| 238 respAnd b1 b2 s = ( left , right ) where | |
| 239 left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true) | |
| 240 left and with b1 s | b2 s | |
| 241 left () | false | false | |
| 242 left () | false | true | |
| 243 left () | true | false | |
| 244 left refl | true | true = ( refl , refl ) | |
| 245 right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true | |
| 246 right ( x1 , x2 ) with b1 s | b2 s | |
| 247 right (() , ()) | false | false | |
| 248 right (() , _) | false | true | |
| 249 right (_ , ()) | true | false | |
| 250 right (refl , refl) | true | true = refl | |
| 251 | |
| 252 PrimSemComm : ∀ {l} -> PrimComm -> Rel State l | |
| 253 PrimSemComm prim s1 s2 = Id State (prim s1) s2 | |
| 254 | |
| 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 |