|
96
|
1 -title: Hoare Logic
|
|
|
2
|
|
|
3 -- files
|
|
|
4
|
|
|
5 Hoare.agda Hoare logic data structre
|
|
|
6 HoareSoundness.agda Hoare logic soundness
|
|
|
7 RelOp.agda Set theoretic operation
|
|
|
8 whileTestPrim.agda definition of simple program and conditions as a Hoare logic command
|
|
|
9 whileTestPrimProof.agda proof using HoareSoundness
|
|
|
10
|
|
|
11 whileTestGears.agda Gears form of proof
|
|
|
12 simple.agda
|
|
|
13 utilities.agda
|
|
|
14
|
|
|
15 -- Hoare logic Programm commands
|
|
|
16
|
|
|
17 data Comm : Set where
|
|
|
18 Skip : Comm
|
|
|
19 Abort : Comm
|
|
|
20 PComm : PrimComm -> Comm
|
|
|
21 Seq : Comm -> Comm -> Comm
|
|
|
22 If : Cond -> Comm -> Comm -> Comm
|
|
|
23 While : Cond -> Comm -> Comm
|
|
|
24
|
|
|
25 -- Example
|
|
|
26
|
|
|
27 record Env : Set where
|
|
|
28 field
|
|
|
29 varn : ℕ
|
|
|
30 vari : ℕ
|
|
|
31
|
|
|
32 program : ℕ → Comm
|
|
|
33 program c10 =
|
|
|
34 Seq ( PComm (λ env → record env {varn = c10})) --- n = c10 ;
|
|
|
35 $ Seq ( PComm (λ env → record env {vari = 0})) --- i = 0 ;
|
|
|
36 $ While (λ env → lt zero (varn env ) ) --- while ( 0 < n ) {
|
|
|
37 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) --- i = i + 1
|
|
|
38 $ PComm (λ env → record env {varn = ((varn env) - 1)} )) --- n = n - 1 }
|
|
|
39
|
|
|
40 This is a syntax tree of a program.
|
|
|
41
|
|
|
42 -- Interpretation of the example
|
|
|
43
|
|
|
44 {-# TERMINATING #-}
|
|
|
45 interpret : Env → Comm → Env
|
|
|
46 interpret env Skip = env
|
|
|
47 interpret env Abort = env
|
|
|
48 interpret env (PComm x) = x env
|
|
|
49 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
|
|
|
50 interpret env (If x then else) with x env
|
|
|
51 ... | true = interpret env then
|
|
|
52 ... | false = interpret env else
|
|
|
53 interpret env (While x comm) with x env
|
|
|
54 ... | true = interpret (interpret env comm) (While x comm)
|
|
|
55 ... | false = env
|
|
|
56
|
|
|
57 -- Hoare logic Programm commands with Post and Pre conditions
|
|
|
58
|
|
|
59 A syntax tree of a program with conditions.
|
|
|
60
|
|
|
61 data HTProof : Cond -> Comm -> Cond -> Set where
|
|
|
62 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
|
|
|
63 (pr : Axiom bPre pcm bPost) ->
|
|
|
64 HTProof bPre (PComm pcm) bPost
|
|
|
65 SkipRule : (b : Cond) -> HTProof b Skip b
|
|
|
66 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
|
|
|
67 HTProof bPre Abort bPost
|
|
|
68 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
|
|
|
69 {bPost' : Cond} -> {bPost : Cond} ->
|
|
|
70 Tautology bPre bPre' ->
|
|
|
71 HTProof bPre' cm bPost' ->
|
|
|
72 Tautology bPost' bPost ->
|
|
|
73 HTProof bPre cm bPost
|
|
|
74 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
|
|
|
75 {cm2 : Comm} -> {bPost : Cond} ->
|
|
|
76 HTProof bPre cm1 bMid ->
|
|
|
77 HTProof bMid cm2 bPost ->
|
|
|
78 HTProof bPre (Seq cm1 cm2) bPost
|
|
|
79 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
|
|
|
80 {bPre : Cond} -> {bPost : Cond} ->
|
|
|
81 {b : Cond} ->
|
|
|
82 HTProof (bPre and b) cmThen bPost ->
|
|
|
83 HTProof (bPre and neg b) cmElse bPost ->
|
|
|
84 HTProof bPre (If b cmThen cmElse) bPost
|
|
|
85 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
|
|
|
86 HTProof (bInv and b) cm bInv ->
|
|
|
87 HTProof bInv (While b cm) (bInv and neg b)
|
|
|
88
|
|
|
89 -- Example of proposition
|
|
|
90
|
|
|
91 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
|
|
|
92 proof1 c10 =
|
|
|
93 SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
|
|
|
94 $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 )
|
|
|
95 $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 (
|
|
|
96 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
|
|
|
97 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
|
|
|
98 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
|
|
|
99
|
|
|
100 This defines a connected sequence of conditions.
|
|
|
101
|
|
|
102 -- Semantics of commands
|
|
|
103
|
|
|
104 SemComm : Comm -> Rel State (Level.zero)
|
|
|
105 SemComm Skip = RelOpState.deltaGlob
|
|
|
106 SemComm Abort = RelOpState.emptyRel
|
|
|
107 SemComm (PComm pc) = PrimSemComm pc
|
|
|
108 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
|
|
|
109 SemComm (If b c1 c2)
|
|
|
110 = RelOpState.union
|
|
|
111 (RelOpState.comp (RelOpState.delta (SemCond b))
|
|
|
112 (SemComm c1))
|
|
|
113 (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
|
|
|
114 (SemComm c2))
|
|
|
115 SemComm (While b c)
|
|
|
116 = RelOpState.unionInf
|
|
|
117 (λ (n : ℕ) ->
|
|
|
118 RelOpState.comp (RelOpState.repeat n
|
|
|
119 (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm c))) (RelOpState.delta (NotP (SemCond b))))
|
|
|
120
|
|
|
121 This defines a proposition of Hoare conditions. It is not proved yet.
|
|
|
122
|
|
|
123 The semantics of while-command is defined as any countable sequence of the body.
|
|
|
124
|
|
|
125 -- Soundness
|
|
|
126
|
|
|
127 Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
|
|
|
128 HTProof bPre cm bPost -> Satisfies bPre cm bPost
|
|
|
129
|
|
|
130 The proof of the soundness of the semantics of HTProof.
|
|
|
131
|
|
|
132 -- An example of the soundness
|
|
|
133
|
|
|
134 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
|
|
|
135
|
|
|
136 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
|
|
|
137 HTProof bPre cm bPost -> Satisfies bPre cm bPost
|
|
|
138 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
|
|
|
139
|
|
|
140 proofOfProgram : (c10 : ℕ) → (input output : Env )
|
|
|
141 → initCond input ≡ true
|
|
|
142 → (SemComm (program c10) input output)
|
|
|
143 → termCond {c10} output ≡ true
|
|
|
144 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem
|
|
|
145
|
