Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestPrim.agda @ 7:e7d6bdb6039d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix test1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Dec 2018 22:35:38 +0900
parents 64bd5c236002
children e4f087b823d4
comparison
equal deleted inserted replaced
6:28e80739eed6 7:e7d6bdb6039d
32 x - zero = x 32 x - zero = x
33 zero - _ = zero 33 zero - _ = zero
34 (suc x) - (suc y) = x - y 34 (suc x) - (suc y) = x - y
35 35
36 lt : ℕ -> ℕ -> Bool 36 lt : ℕ -> ℕ -> Bool
37 lt x y with (suc x ) ≤? y 37 lt x y with suc x ≤? y
38 lt x y | yes p = true 38 lt x y | yes p = true
39 lt x y | no ¬p = false 39 lt x y | no ¬p = false
40 40
41 Equal : ℕ -> ℕ -> Bool 41 Equal : ℕ -> ℕ -> Bool
42 Equal x y with x ≟ y 42 Equal x y with x ≟ y
45 45
46 program : Comm 46 program : Comm
47 program = 47 program =
48 Seq ( PComm (λ env → record env {varn = 10})) 48 Seq ( PComm (λ env → record env {varn = 10}))
49 $ Seq ( PComm (λ env → record env {vari = 0})) 49 $ Seq ( PComm (λ env → record env {vari = 0}))
50 $ While (λ env → lt (varn env ) zero ) 50 $ While (λ env → lt zero (varn env ) )
51 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) 51 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
52 $ PComm (λ env → record env {varn = ((varn env) - 1)} )) 52 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
53 53
54 simple : Comm 54 simple : Comm
55 simple = 55 simple =
69 ... | true = interpret (interpret env comm) (While x comm) 69 ... | true = interpret (interpret env comm) (While x comm)
70 ... | false = env 70 ... | false = env
71 71
72 test1 : Env 72 test1 : Env
73 test1 = interpret ( record { vari = 0 ; varn = 0 } ) program 73 test1 = interpret ( record { vari = 0 ; varn = 0 } ) program
74
75 tests : Env
76 tests = interpret ( record { vari = 0 ; varn = 0 } ) simple
74 77
75 78
76 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 79 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true
77 empty-case _ = refl 80 empty-case _ = refl
78 81
159 proof1 = 162 proof1 =
160 SeqRule {λ e → true} ( PrimRule empty-case ) 163 SeqRule {λ e → true} ( PrimRule empty-case )
161 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) 164 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 )
162 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( 165 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 (
163 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} 166 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
164 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt (varn e) zero } lemma3) 167 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
165 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 168 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
166 where 169 where
167 lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond 170 lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
168 lemma1 env with stmt1Cond env 171 lemma1 env with stmt1Cond env
169 lemma1 env | false = refl 172 lemma1 env | false = refl
170 lemma1 env | true = refl 173 lemma1 env | true = refl
172 lemma2 env with stmt2Cond env | Equal (varn env + vari env) 10 175 lemma2 env with stmt2Cond env | Equal (varn env + vari env) 10
173 lemma2 env | false | false = refl 176 lemma2 env | false | false = refl
174 lemma2 env | false | true = refl 177 lemma2 env | false | true = refl
175 lemma2 env | true | true = refl 178 lemma2 env | true | true = refl
176 lemma2 env | true | false = {!!} 179 lemma2 env | true | false = {!!}
177 lemma3 : Axiom (whileInv /\ (λ env → lt (varn env) zero)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' 180 lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
178 lemma3 = {!!} 181 lemma3 = {!!}
179 lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv 182 lemma4 : Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
180 lemma4 = {!!} 183 lemma4 = {!!}
181 lemma5 : Tautology (whileInv /\ neg (λ z → lt (varn z) zero)) termCond 184 lemma5 : Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond
182 lemma5 = {!!} 185 lemma5 = {!!}
183 186
184 187