Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTest.agda @ 2:b05a4156da01

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add HTProof
author ryokka
date Thu, 13 Dec 2018 19:05:43 +0900
parents ab73094377a2
children
comparison
equal deleted inserted replaced
1:ab73094377a2 2:b05a4156da01
3 open import Data.Nat 3 open import Data.Nat
4 open import Data.Bool hiding (_≟_) 4 open import Data.Bool hiding (_≟_)
5 open import Data.Product 5 open import Data.Product
6 open import Relation.Nullary 6 open import Relation.Nullary
7 open import Relation.Binary 7 open import Relation.Binary
8 open import Relation.Binary.PropositionalEquality
8 open import SET 9 open import SET
9 10 import Level
10 11
11 record Env : Set where 12 record Env : Set where
12 field 13 field
13 varn : ℕ 14 varn : ℕ
14 vari : ℕ 15 vari : ℕ
15 open Env 16 open Env
16 17
18 PrimComm = Env → Env
19
20 Cond = Env → Bool
21
17 neg : (Env → Bool) → (Env → Bool) 22 neg : (Env → Bool) → (Env → Bool)
18 neg x e = not (x e) 23 neg x e = not (x e)
19 24
20 and : (Env → Bool) → (Env → Bool) → (Env → Bool) 25 and : (Env → Bool) → (Env → Bool) → (Env → Bool)
21 and x y e = (x e) ∧ (y e) 26 and x y e = (x e) ∧ (y e)
22 27
23 enveq : (Env → Bool) → (Env → Bool) → Set 28 data Comm : Set where
24 enveq x y = {!!} 29 Skip : Comm
30 Abort : Comm
31 PComm : PrimComm -> Comm
32 Seq : Comm -> Comm -> Comm
33 If : Cond -> Comm -> Comm -> Comm
34 While : Cond -> Comm -> Comm
25 35
26 sem : (Env → Bool) → Pred Env 36 data HTProof : Cond -> Comm -> Cond -> Set (Level.suc (Level.suc Level.zero)) where
27 sem x y = {!!} 37 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
38 (pr : Cond -> PrimComm -> Cond -> Set (Level.suc Level.zero)) ->
39 HTProof bPre (PComm pcm) bPost
40 SkipRule : (b : Cond) -> HTProof b Skip b
41 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
42 HTProof bPre Abort bPost
43 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
44 {bPost' : Cond} -> {bPost : Cond} ->
45 bPre ≡ bPre' ->
46 HTProof bPre' cm bPost' ->
47 bPost' ≡ bPost ->
48 HTProof bPre cm bPost
49 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
50 {cm2 : Comm} -> {bPost : Cond} ->
51 HTProof bPre cm1 bMid ->
52 HTProof bMid cm2 bPost ->
53 HTProof bPre (Seq cm1 cm2) bPost
54 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
55 {bPre : Cond} -> {bPost : Cond} ->
56 {b : Cond} ->
57 HTProof (and bPre b) cmThen bPost ->
58 HTProof (and bPre (neg b)) cmElse bPost ->
59 HTProof bPre (If b cmThen cmElse) bPost
60 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
61 HTProof (and bInv b) cm bInv ->
62 HTProof bInv (While b cm) (and bInv (neg b))
63 Rule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> {w : Cond} ->
64 HTProof w cm bInv ->
65 HTProof bInv (While b cm) (and bInv (neg b))
28 66
29 tautValid : (b1 b2 : Env → Bool) -> enveq b1 b2 ->
30 (s : Env) -> sem b1 s -> sem b2 s
31 tautValid = {!!}
32
33 respNeg : (b : Env → Bool) -> (s : Env) ->
34 Iff (sem (neg b) s) (¬ sem b s)
35 respNeg = {!!}
36
37 respAnd : (b1 b2 : Env → Bool) -> (s : Env) ->
38 Iff (sem (and b1 b2) s)
39 ((sem b1 s) × (sem b2 s))
40 respAnd = {!!}
41
42 PrimSemComm : ∀ {l} -> (Env → Env) -> Rel Env l
43 PrimSemComm = {!!}
44
45 Axiom :( Env → Bool) -> (Env → Env) -> (Env → Bool) -> Set
46 Axiom = {!!}
47
48 axiomValid : ∀ {l} -> (bPre : Env → Bool ) -> (pcm : (Env → Env)) -> (bPost : Env → Bool) ->
49 (ax : Axiom bPre pcm bPost) -> (s1 s2 : Env) ->
50 sem bPre s1 -> PrimSemComm {l} pcm s1 s2 -> sem bPost s2
51 axiomValid = {!!}
52
53 open import Hoare (Env → Bool) (Env → Env) neg and enveq Env sem tautValid
54 respNeg respAnd PrimSemComm Axiom axiomValid
55 67
56 lt : ℕ → ℕ → Bool 68 lt : ℕ → ℕ → Bool
57 lt x y with x <? y 69 lt x y with x <? y
58 lt x y | yes p = true 70 lt x y | yes p = true
59 lt x y | no ¬p = false 71 lt x y | no ¬p = false
96 initCond _ = true 108 initCond _ = true
97 109
98 termCond : Env → Bool 110 termCond : Env → Bool
99 termCond env = (vari env) == 10 111 termCond env = (vari env) == 10
100 112
113 iff : Bool → Bool → Bool
114 iff true true = true
115 iff false false = true
116 iff _ _ = false
117
118 proposition1 : Cond → PrimComm → Cond → Env → Set
119 proposition1 pre cmd post = λ (env : Env) → {!!} -- iff (pre env) (post (cmd env))
101 120
102 proof1 : HTProof initCond program termCond 121 proof1 : HTProof initCond program termCond
103 proof1 = {!!} 122 proof1 = SeqRule (PrimRule {!!} )
123 (SeqRule (PrimRule {!!} )
124 (Rule {!!} (WhileRule ?)))
104 125