-
Notifications
You must be signed in to change notification settings - Fork 2
/
hoarelogicsemantics.v
220 lines (163 loc) · 7.41 KB
/
hoarelogicsemantics.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
(** * Semantics of my Hoare Logic
This file is part of the "Tutorial on Hoare Logic".
For an introduction to this Coq library,
see README #or <a href=index.html>index.html</a>#.
*)
Set Implicit Arguments.
(** * Expression Language
My Hoare logic is parametrized by the expression language.
The language is here assumed to have global variables.
Furthermore, expressions are purely functional (they terminates
and have no side effects). However, expressions and variables are
strongly-typed. Here, this typing is directly performed by Coq.
- "[Var A]" is the type of variables storing values of type [A]
- "[Expr A]" is the type of expressions return values of type [A]
- [Env] is the type of environment. An environment is a mapping from variables into values.
- "[upd x v e]" sets [v] as the new value of [x] from environment [e]
- [eval] evaluates an expression in a given environment.
See the file #<a href="exgcd.html">#[exgcd]#</a># to get a simple example
of how such a language can be instantiated.
*)
Module Type ExprLang.
Parameter Var: Type -> Type.
Parameter Expr: Type -> Type.
Parameter Env: Type.
Parameter upd: forall (A:Type), (Var A) -> A -> Env -> Env.
Parameter eval: forall (A:Type), (Expr A) -> Env -> A.
End ExprLang.
(** * Definitions of my Hoare logic *)
Module Type HoareLogicDefs.
Declare Module E: ExprLang.
(** ** The programming language: syntax and semantics *)
(** Abstract syntax of the imperative programming language
- [Iskip] is an instruction to "do nothing"
- "[Iset x expr]" stores in [x] the result of [expr]
- [Iif] represents conditional branching
- [Iseq] represents the sequence of two instructions
- [Iwhile] represents the while-loop
This semantics is formalizes by [exec] predicate below.
*)
Inductive ImpProg: Type :=
| Iskip: ImpProg
| Iset (A:Type) (x:E.Var A) (expr:E.Expr A): ImpProg
| Iif (cond:E.Expr bool) (p1 p2:ImpProg): ImpProg
| Iseq (p1 p2:ImpProg): ImpProg
| Iwhile (cond:E.Expr bool) (p:ImpProg): ImpProg.
(** The semantics of the programming language is given by the following natural semantics.
Here "[exec e0 p e1]" means that "in the initial environment [e0] the execution of [p]
terminates in the final environment [e1]".
*)
Inductive exec: E.Env -> ImpProg -> E.Env -> Prop :=
| exec_Iskip:
forall e, (exec e Iskip e)
| exec_Iset:
forall (A:Type) e x (expr: E.Expr A),
(exec e (Iset x expr) (E.upd x (E.eval expr e) e))
| exec_Iif:
forall e (cond: E.Expr bool) p1 p2 e',
(exec e (if (E.eval cond e) then p1 else p2) e')
-> (exec e (Iif cond p1 p2) e')
| exec_Iseq:
forall e p1 p2 e' e'',
(exec e p1 e')
-> (exec e' p2 e'')
-> (exec e (Iseq p1 p2) e'')
| exec_Iwhile:
forall e cond p e',
(exec e (Iif cond (Iseq p (Iwhile cond p)) Iskip) e')
-> (exec e (Iwhile cond p) e').
(** This language is thus deterministic.
This is proved by lemma [exec_deterministic] in file
#<a href="totalhoarelogic.html">#[totalhoarelogic]#</a>#.
*)
(** ** The specification language: syntax and semantics
If [prog] is a program, [pre] a precondition (i.e. a required
property on the initial environment) and [post] a postcondition
(i.e. a property on the final environment that [prog] must ensure
when [pre] is initially satisfied), then a specification in Hoare
logic is written:
- "[pre |= prog {= post =}]" in partial correctness (i.e. even if
[pre] is satisfied, [prog] may not terminate)
- "[pre |= prog [= post =]]" in total correctness (i.e. when [pre]
is satisfied, [prog] must terminate).
Below, we give the semantics of these notations. Here the assertion
language is shallow embedded (there is no syntax for it: we use
directly the Coq proposition language).
[Pred] is the type of assertions.
*)
Definition Pred := E.Env -> Prop.
(** Deduction operator "|=" is here only a syntactic sugar.
In the following, [p |= q] can also be read "[q] is weaker than [p]".
*)
Notation "p |= q" := (forall e, (p e) -> (q e)) (at level 80, no associativity).
(** [wlp] represents the Weakest Liberal Precondition (i.e.
"[wlp prog post]" is the weakest condition on the initial environment ensuring
that [post] is ensured on any final environment of [prog], when such environment
exists)
*)
Definition wlp: ImpProg -> Pred -> Pred
:= fun prog post e => (forall e', (exec e prog e') -> (post e')).
Notation "p {= post =}" := (wlp p post) (at level 70).
(** [wp] represents the Weakest Precondition (i.e. "[wp prog post]" is
the weakest condition on the initial environment ensuring that there
exists a final environment of [prog] satisfying [post]). Here as the language is
deterministic, I proved that "[(wp prog post) |= (wlp prog post)]"
see lemma [wp_entails_wlp] below.
*)
Definition wp: ImpProg -> Pred -> Pred
:= fun prog post e => exists e', (exec e prog e') /\ (post e').
Notation "p [= post =]" := (wp p post) (at level 70).
(** ** A useful base of hints
These hints are used in the metatheoritical proofs of the logic.
*)
Global Hint Resolve exec_Iskip exec_Iset exec_Iif exec_Iseq exec_Iwhile: hoare.
Parameter exec_Iif_true:
forall e cond p1 p2 e',
(E.eval cond e)=true
-> (exec e p1 e')
-> (exec e (Iif cond p1 p2) e').
Parameter exec_Iif_false:
forall e cond p1 p2 e',
(E.eval cond e)=false
-> (exec e p2 e')
-> (exec e (Iif cond p1 p2) e').
Global Hint Resolve exec_Iif_true exec_Iif_false: hoare.
End HoareLogicDefs.
(** * Generation of proof obligations (POs)
Given [sem_wp] one of the two preceding notion of
weakest-precondition, the generation of proof obligations is a
function [synt_wp] logically equivalent to [sem_wp], which proceeds
recursively on the abstract syntax of the program. Hence,
"[synt_wp prog post]" is an assertion which does not involve [exec].
In practice, the PO generation is run by invoking the [soundness] lemma.
The [completeness] lemma is only ensuring that if the generated PO
seems hard to prove, this is not due to a bug in [synt_wp]
implementation.
*)
Module Type HoareProofSystem.
Declare Module HLD: HoareLogicDefs.
Import HLD.
Parameter sem_wp: ImpProg -> Pred -> Pred.
Parameter synt_wp: ImpProg -> Pred -> Pred.
Parameter soundness: forall pre p post, pre |= (synt_wp p post) -> pre |= (sem_wp p post).
Parameter completeness: forall pre p post, pre |= (sem_wp p post) -> pre |= (synt_wp p post).
End HoareProofSystem.
(** * The whole meta-theory
The whole meta-theory is described by this module signature. This signature is implemented in file #<a href="hoarelogic.html">#[hoarelogic]#</a>#.
See the file #<a href="exgcd.html">#[exgcd]#</a># to get a simple example
of how the "proof obligation generation" is used.
- module [PHL] contains the PO generation in partial correctness.
- module [THL] contains the PO generation in total correctness.
*)
Module Type HoareLogicSem.
Declare Module E: ExprLang.
Declare Module HLD: HoareLogicDefs with Module E:=E.
Import HLD.
Declare Module PHL: HoareProofSystem with Module HLD:=HLD with Definition sem_wp:=wlp.
Declare Module THL: HoareProofSystem with Module HLD:=HLD with Definition sem_wp:=wp.
Parameter wp_entails_wlp: forall prog post, prog [= post =] |= prog {= post =}.
End HoareLogicSem.
(** "Tutorial on Hoare Logic" Library. Copyright 2007 Sylvain Boulme.
This file is distributed under the terms of the
"GNU LESSER GENERAL PUBLIC LICENSE" version 3.
*)