MPRI 2.7.1 - Projet Coq
2017-2018
On se propose ici de développer en Coq un calcul de plus petite condition pour le langage While.
Cette procédure sera prouvée correcte en Coq et extraite vers le langage OCaml.
1 Le langage While
Définition 1.1 (c.p.o. pointé). Soit X un ensemble. On dénote par X
⊥
le c.p.o. pointé (X ∪ {⊥}, )
où ⊥ est symbole arbitraire que l’on suppose frais (notamment ⊥ /∈ X) et est le plus petit pré-ordre
sur X ∪ {⊥} t.q. ∀x ∈ X. ⊥ x. Ainsi défini, X
⊥
est un ω-c.p.o.
Définition 1.2 (Langage While). Soit X = {x, y, . . .} un ensemble infini dénombrable de variables de
programme et E = {e, . . .} un ensemble d’expressions de programme. La syntaxe du langage While est
définie comme suit :
s ::= skip (no-op)
| abort (arrêt)
| x ← e (affectation)
| s; s (séquence)
| if (e) then s else s (conditionnelle)
| while (e) do s (boucle while)
On écrit if (e) then s pour if (e) then s else skip.
Définition 1.3 (Sémantique). Une mémoire est une fonction de X dans Z. On dénote par M = {m, . . .}
l’ensemble de toutes les mémoires. Pour une mémoire m ∈ M, une variable x ∈ X et une valeur z ∈ Z,
on écrit m[x ← z] pour la mémoire définie par :
(
m[x ← z](y) = z si x = y
m[x ← z](y) = m(y) sinon.
On se donne également une fonction JeK
m
∈ Z d’interprétation des expressions. La sémantique JsK d’un
programme While est une fonction de M
⊥
dans M
⊥
définie inductivement sur la structure de s :
JsK(⊥) = ⊥ JskipK(m) = m
JabortK(m) = ⊥ Jx ← eK(m) = m[x ← JeK
m
]
Js
1
; s
2
K(m) = Js
2
K(Js
1
K(m)) Jwhile (e) do sK =
G
n∈N
Js
n
¬e
K(m)
Jif (e) then s
1
else s
2
K(m) =
Js
1
K(m) si JeK
m
6= 0
Js
2
K(m) sinon
où s
n
= s; · · · ; s (n fois), s
n
¬e
= ((if (e) then s)
n
; if (e) then abort) et
F
n∈N
α
n
est le plus petit
majorant de la ω-chaîne {α
n
}
n∈N
(ici, sur M
⊥
).
Lemme 1.4. La définition précédente est correcte.
Démonstration. Par induction sur s. Le cas délicat est celui de la boucle while. La preuve se fait en
montrant que {s
n
¬e
}
n∈N
est une ω-chaîne, prouvant de facto l’existence du plus petit majorant.
Lemme 1.5 (Equation de point-fixe). Soit s un programme et e une expression. Alors
Jwhile (e) do sK(m) = Jif (e) then s; while (e) do sK(m).
Notamment, Jwhile (e) do sK(m) =
F
n∈N
Js
n+p
¬e
K(m) pour n’importe quel p ∈ N arbitraire.
Démonstration. Conséquence immédiate de la définition de la sémantique de la boucle while en tant
que plus petit point-fixe de n 7→ Js
n
¬e
K(m).
Lemme 1.6 (Terminaison certaine). Soit s un programme, e une expression et m une mémoire t.q.
Jwhile (e) do sK(m) 6= ⊥. Alors, il existe un entier n t.q. i) Js
n
K(m) |= ¬e, ii) ∀p < n. Js
p
K(m) |= e et
iii) Jwhile (e) do sK(m) = Js
n
K(m) — où pour m ∈ M
⊥
, m |= e ssi m 6= ⊥ ∧JeK(m) 6= 0.
Démonstration. Soit E = {n ∈ N | J(if (e) then s)
n
K(m) |= ¬e}. Si E est vide, alors pour tout n ∈ N,
Js
n
¬e
K(m) = ⊥. Ainsi, Jwhile (e) do sK(m) = ⊥, ce qui contredit les hypothèses du lemme. Ainsi, E
est non vide. Soit n le plus petit élément de E. Tout d’abord, on montre que pour tout p ≤ n, on a
J(if (e) then s)
p
K(m) = Js
p
K(m). Si p = 0, c’est immédiate. Si p = k + 1 > 0, alors
J(if (e) then s)
k+1
K = Jif (e) then sK(J(if (e) then s)
k
K(m)
| {z }
|= e par minimalité de n
)
= JsK(J(if (e) then s)
k
K(m)
| {z }
= Js
k
K(m) par I.H.
= Js
k+1
K(m),
ce qui termine l’induction. Ainsi, de ce qui précède et par minimalité de n, Js
n
K(m) |= ¬e et Js
p
K(m) |= e
pour tout p < n. Maintenant, pour n’importe quel l ∈ N, nous avons
Js
n+l
¬e
K(m) = Js
l
¬e
K(J(if (e) then s)
n
K(m)
| {z }
|= ¬e par définition de n
)
= Js
0
¬e
K(J(if (e) then s)
n
K) (induction sur l)
= Jif (e) then abortK(J(if (e) then s)
n
(m)K
| {z }
|= ¬e par définition de n
)
= J(if (e) then s)
n
K(m) = Js
n
K(m).
Ainsi, Jwhile (e) do sK(m) =
F
l∈N
Js
l
¬e
K(m) =
F
l∈N
Js
n+l
¬e
K(m) =
F
l∈N
Js
n
K(m) = Js
n
K(m).
Définition 1.7 (Assertion). On appelle assertion toute partie (ou sous-ensemble) de M et on écrit
A = {φ, ψ, . . .} pour l’ensemble des assertions. La notion de validité d’une assertion est réduite à celle
d’appartenance ensembliste : m |= φ ssi m ∈ φ. Il est usuel décrire |= φ pour ∀m ∈ M. m |= φ. On
définit les connecteurs suivants sur les assertions :
> , M ⊥ , ∅
¬φ , φ
{
φ ∧ ψ , φ ∩ ψ
φ ∨ ψ , φ ∪ ψ φ =⇒ ψ , ¬φ ∨ ψ
∀x. φ , {m | ∀z ∈ Z. m[x ← z] |= φ}
∃x. φ , {m | ∃z ∈ Z. m[x ← z] |= φ}.
La notion de validité et de satisfiabilité est réifié au niveau des assertions :
∀m. φ , > si ∀m. m |= φ, ⊥ sinon
∃m. φ , > si ∃m. m |= φ, ⊥ sinon
On définit également une notion de substitution pour les assertions :
φ[x ← z] , {m | m[x ← z] |= φ}
φ[x ← e] , {m | m[x ← JeK
m
] |= φ}.
Enfin, toute expression e définit une assertion ˆe comme suit :
ˆe , {m ∈ M | JeK
m
6= 0}.
On confond ˆe et e quand le contexte le permet.
2
Skip
` {φ} skip {φ}
Abort
` {φ} abort {ψ}
Assgn
` {φ[x ← e]} x ← e {φ}
Conseq
φ =⇒ φ
0
ψ
0
=⇒ ψ ` {φ
0
} s {ψ
0
}
` {φ} s {ψ}
Seq
` {φ} s
1
{ξ} ` {ξ} s
2
{ψ}
` {φ} s
1
; s
2
{ψ}
If
` {φ ∧ e} s
1
{ψ} ` {φ ∧ ¬e} s
2
{ψ}
` {φ} if (e) then s
1
else s
2
{ψ}
While
` {I ∧ e} s {I}
` {I} while (e) do s {I ∧ ¬e}
Figure 1 – Règles de Hoare
2 Triplet de Hoare
Définition 2.1 (Triplet de Hoare). Un triplet de Hoare est la donnée de deux assertions φ et ψ (la
pré- et la post-condition) et d’un programme s t.q.
∀m |= φ. JsK(m) |=
⊥
ψ.
où m |=
⊥
φ ssi m = ⊥ ou m |= φ. On note ce triplet |= {φ} s {ψ}.
Définition 2.2 (Notion de prouvabilité pour Hoare). La Figure 1 définit inductivement une relation
` {φ} s {ψ} où φ et ψ sont des assertions et s un programme.
Theorème 2.3. Si ` {φ} s {ψ} alors |= {φ} s {ψ}.
Démonstration. On prouve |= {φ} s {ψ} par induction sur ` {φ} s {ψ} et par analyse de case sur la
dernière règle utilisée dans ` {φ} s {ψ}. On utilise les notations de la Figure 1.
[Skip] Soit m |= φ. Alors, JskipK(m) = m et JskipK(m) |= φ par hypothèse, donc JskipK(m) |=
⊥
φ.
[Abort] Soit m |= φ. Alors JabortK(m) |=
⊥
ψ est toujours vrai car JabortK(m) = ⊥.
[Assign] Soit m |= φ[x ← e] (ou encore, de manière équivalente m |= φ[x ← JeK
m
]). On veut montrer
que Jx ← eK |=
⊥
φ. Or, Jx ← eK = m[x ← JeK
m
], et par définition de φ[x ← e], m[x ← JeK
m
] |= φ. Donc
Jx ← eK |=
⊥
φ.
[Conseq] Soit m |= φ. On veut montrer que JsK(m) |=
⊥
ψ. Par l’hypothèse |= φ =⇒ φ
0
, on sait que
m |= φ
0
. Or, par hypothèse d’induction, on sait également que |= {φ
0
} s {ψ
0
}. Donc JsK(m) |=
⊥
ψ
0
.
Finalement, de l’hypothèse |= ψ
0
=⇒ ψ, on conclut que JsK(m) |=
⊥
ψ.
[Seq] Soit m |= φ. On veut montrer que Js
1
; s
2
K(m) |=
⊥
ψ. Si Js
1
; s
2
K(m) = ⊥, c’est immédiat. Sinon,
par la première hypothèse d’induction, on sait que |= {φ} s
1
{ξ}, et donc Js
1
K(m) |=
⊥
ξ. Nécessairement,
comme Js
1
; s
2
K(m) 6= ⊥, Js
1
K(m) 6= ⊥. Ainsi, Js
1
K(m) |= ξ. Maintenant, par la seconde hypothèse
d’induction, on a |= {ξ} s
2
{ψ}. Donc, Js
2
K(Js
1
K(m)) |= ψ (et Js
2
K(Js
1
K(m)) |=
⊥
ψ). On conclut en
remarquant que Js
2
K(Js
1
K(m)) = Js
1
; s
2
K(m).
[If] Soit m |= φ. On veut prouver que Jif (e) then s
1
else s
2
K(m) |= ψ. Supposons que JeK
m
6= 0. Alors,
m |= φ ∧ ˆe, et par la première hypothèse d’induction, nous avons Js
1
K(m) |=
⊥
ψ. Or, comme JeK
m
6= 0,
nous avons également que Jif (e) then s
1
else s
2
K(m) = Js
1
K(m), ce qui nous permet de conclure. Le
cas JeK
m
= 0 est similaire et utilise la seconde hypothèse d’induction.
[While] Soit m |= I. On veut prouver que Jwhile (e) do sK(m) |=
⊥
I∧¬e. Si Jwhile (e) do sK(m) = ⊥,
c’est immédiat. Sinon par le Lemme 1.6, on sait qu’il existe un certain n ∈ N t.q. i) Js
n
K(m) |= ¬e,
ii) ∀p < n. Js
p
K(m) |= e et iii) Jwhile (e) do sK(m) = Js
n
K(m). On prouve maintenant par induction sur
n que Js
n
K(m) |= I. Si n = 0, c’est immédiat car Js
0
K(m) = m |= I. Si n = p + 1 > 0, alors par hypothèse
d’induction interne, Js
p
K(m) |= I. Par hypothèse sur n, on sait que Js
p
K(m) |= e. Ainsi, Js
p
K(m) |= I ∧ e,
et par hypothèse d’induction externe, on obtient JsK(Js
p
K(m)) |= I. On termine l’induction interne en
remarquant que JsK(Js
p
K(m)) = Js
n
K(m). Enfin, par propriété sur n, on sait que Js
n
K(m) |= ¬e. Ainsi,
Js
n
K(m) |= I ∧ ¬e, ou encore Jwhile (e) do sK(m) |=
⊥
I ∧ ¬e.
3
3 Calcul de plus petite précondition
Définition 3.1 (Plus petite précondition). Soit s un programme et φ une assertion. On suppose que toute
boucle while (e) do s
0
de s est décorée d’un invariant I ∈ A, décoration que l’on note while
I
(e) do s
0
.
La plus petite précondition de φ pour s, notée wp
?
(s, φ), est définie inductivement comme suit :
wp
?
(skip, φ) , φ wp
?
(abort, φ) , >
wp
?
(x ← e, φ) , φ[x ← e] wp
?
(s
1
; s
2
, φ) , wp
?
(s
1
, wp
?
(s
2
, φ))
wp
?
(if (e) then s
1
else s
2
, φ) ,
(e =⇒ wp
?
(s
1
, φ)) ∧ (¬e =⇒ wp
?
(s
2
, φ))
wp
?
(while
I
(e) do s, φ) ,
I
∧ ∀m. (e ∧ I =⇒ wp
?
(s, I))
∧ ∀m. (¬e ∧ I =⇒ φ)
Theorème 3.2. Il est toujours vrai que |= {wp
?
(s, ψ)} s {ψ}. Notamment, si |= φ =⇒ wp
?
(s, ψ),
alors |= {φ} s {ψ}.
Démonstration. On prouve par induction sur s que |= {wp
?
(s, ψ)} s {ψ}. On ne détaille que le cas pour
la boucle while, les autres cas étant immédiats. Supposons que s = while
I
(e) do s
0
et soit m t.q.
m |= wp
?
(s, φ). Notons que de cette dernière propriété, nous avons que |= e ∧ I =⇒ wp
?
(s, I) et
|= ¬e ∧ I =⇒ φ. Nous voulons montrer que JsK(m) |=
⊥
φ. Si JsK(m) = ⊥, alors JsK(m) |=
⊥
φ par
définition et la preuve est finie. Sinon, par le Lemme 1.6, il existe un n ∈ N t.q. JsK(m) = J(s
0
)
n
K(m),
J(s
0
)
n
K |= ¬e et ∀p < n. J(s
0
)
p
K(m) |= e. Nous prouvons par induction sur n que J(s
0
)
n
K |= φ. Si n = 0,
alors m |= ¬e. De plus, de m |= wp
?
(s, φ), on a m |= I et nous savons que |= ¬e ∧ I =⇒ φ. Ainsi,
m |= φ. Si maintenant n = p + 1 > 0, alors par hypothèse d’induction interne, J(s
0
)
p
K(m) |= I. Posons
m
p
, J(s
0
)
p
K(m). Par hypothèse sur n, nous savons également que m
p
|= e. Ainsi, de |= e ∧ I =⇒
wp
?
(s, I), nous obtenons que m
p
|= wp
?
(s
0
, I). Par hypothèse d’induction externe, nous obtenons que
Js
0
K(m
p
) |= I, i.e. que J(s
0
)
n
K(m) |= I. Par définition de n, J(s
0
)
n
K(m) |= ¬e. Ainsi, de |= ¬e ∧ I =⇒ φ,
nous avons J(s
0
)
n
K(m) |= φ, ce qui termine l’induction interne et le cas pour while — nous avons prouvé
que JsK(m) |=
⊥
φ.
4 Travail à faire
On vous demande de
1. Définir en Coq la syntaxe du langage
While — le langage des expressions pourra
être laissé abstrait en prenant n’importe
quelle fonction de mem dans int, i.e. du type
des mémoires dans le type des entiers relatifs.
2. Définir en Coq la sémantique des pro-
grammes de While. On pourra dans un pre-
mier temps axiomatiser la théorie des c.p.o.
3. Définir En Coq la notion de validité et de
provabilité pour Hoare — une assertion sera
alors une fonction de mem dans Prop.
4. Démontrer en Coq le Théorème 2.3.
5. Définir en Coq une fonction wp qui cal-
cule la plus petite précondition d’une asser-
tion φ pour un programme s. Cette dernière
échouera dans un premier temps lorsque s
comporte une boucle.
6. Démontrer en Coq que votre fonction wp de
calcul de plus petite précondition est correcte,
i.e. le Théorème 3.2.
7. Définir en Coq une syntaxe pour les asser-
tions et leur interprétation en tant qu’asser-
tion logique. Écrire une fonction wps qui cal-
cule la plus petite précondition d’une asser-
tion syntaxique φ pour un programme s.
8. Comme pour wp, montrer que wps est cor-
recte. On pourra se ramener à la preuve de
correction de wp.
9. Concevoir un mécanisme permettant de don-
ner les invariants de boucle nécessaires au
calcul de plus petite précondition pour les
boucles. Étendre vos fonctions wp et wps en
conséquence, ainsi que leurs preuves de cor-
rection.
4
10. Extraire à partir de votre développement
Coq une fonction OCaml de calcul de plus
petite précondition. Que dire de cette der-
nière ?
5
