header "Condiciones de verificación"
theory VCG_b imports Hoare_b begin
text{* Condiciones de verificación:
El objetivo es transformar la noción de demostrabilidad en la
Lógica de Hoare en demostrabilidad de asertos (predicados sobre
estados).
Dada una terna {P}c{Q}, veremos cómo obtener un aserto A tal que,
⊢ {P}c{Q} si y sólo si A es demostrable (en HOL)
El aserto A se denomina una condición de verificación, y la
función que lo calcula, un generador de condición de verificación
(o VCG).
*}
text{* Para calcular una condición de verificación simulamos la
aplicación de las reglas de la Lógica de Hoare hacia atrás,
recopilando los asertos que deben verificarse. En cuanto al
invariante del bucle While, es necesario proporcionárselo.
Para ello, introducimos la noción de instrucción anotada: análoga
a las instrucciones, donde la instrucción While está anotada con
un invariante I.
*}
datatype acom =
Askip ("SKIP") |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
Aseq acom acom ("_;;/ _" [60, 61] 60) |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
Awhile assn bexp acom ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61)
notation com.SKIP ("SKIP")
text{* Traducción de instrucciones anotadas a instrucciones,
eliminando todas las anotaciones.
*}
fun strip :: "acom ⇒ com" where
"strip SKIP = SKIP" |
"strip (x ::= a) = (x ::= a)" |
"strip (C⇩1;; C⇩2) = (strip C⇩1;; strip C⇩2)" |
"strip (IF b THEN C⇩1 ELSE C⇩2) = (IF b THEN strip C⇩1 ELSE strip C⇩2)" |
"strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
text{* Notación: los elementos de acom (instrucciones anotadas)
los escribiremos con mayúscula; y los elementos de com (instrucciones)
con minúscula.
*}
text{* Precondición más débil para instrucciones anotadas: la definimos
directamente para cada uno de los casos. *}
fun pre :: "acom ⇒ assn ⇒ assn" where
"pre SKIP Q = Q" |
"pre (x ::= a) Q = (λs. Q(s(x := aval a s)))" |
"pre (C⇩1;; C⇩2) Q = pre C⇩1 (pre C⇩2 Q)" |
"pre (IF b THEN C⇩1 ELSE C⇩2) Q =
(λs. if bval b s then pre C⇩1 Q s else pre C⇩2 Q s)" |
"pre ({I} WHILE b DO C) Q = I"
text{* Observación: la precondición más débil de la instrucción
While anotada es precisamente el invariante especificado por
la anotación.
*}
text{* Generador de una condición de verificación: *}
fun vc :: "acom ⇒ assn ⇒ bool" where
"vc SKIP Q = True" |
"vc (x ::= a) Q = True" |
"vc (C⇩1;; C⇩2) Q = (vc C⇩1 (pre C⇩2 Q) ∧ vc C⇩2 Q)" |
"vc (IF b THEN C⇩1 ELSE C⇩2) Q = (vc C⇩1 Q ∧ vc C⇩2 Q)" |
"vc ({I} WHILE b DO C) Q =
((∀s. (I s ∧ bval b s ⟶ pre C I s) ∧
(I s ∧ ¬ bval b s ⟶ Q s)) ∧
vc C I)"
text{* Ejemplo: consideremos el ejemplo siguiente
W : {I} WHILE 0 < x DO C
C: y:= y + x;; x := x-1
I: y + sum x = sum n
Q: y = sum n
En este caso, conocemos que el programa W verifica lo siguiente:
⊢ {λs. s ''x'' = n} ''y'' ::= N 0;; wsum {λs. s ''y'' = sum n}
En la prueba que realizamos aplicando las reglas de la Lógica de
Hoare, el invariante proporcionado fué:
P = "λs. (s ''y'' = sum n - sum(s ''x''))"
Calculamos vc W Q, sin tener en cuenta la inicialización de y a 0.
vc W Q = ((I ∧ x < 0 ⟶ pre C I) ∧
(I ∧ ¬(0 < x) ⟶ Q) ∧
(vc C I))
Por otra parte,
pre C I = pre (y:= y+x) (pre (x:= x-1) I)
= pre (y:= y+x) (I[x-1/x])
= I[x-1/x][y+x/y] = (y+x+ sum (x-1) = sum n)
vc C I = (vc (y:= y+x) (pre (x:= x-1) I)) ∧ (vc (x:x-1) I)
= True ∧ True
= True
Por tanto,
vc W Q = ((I ∧ x < 0 ⟶ I[x-1/x][y+x/y]) ∧
(I ∧ ¬(0 < x) ⟶ Q)
que son las mismas condiciones necesarias para probar en
la Lógica de Hoare la terna {I] wsum {y = sum n}.
*}
text {* Adecuación: VCG es adecuada con respecto a la Lógica
de Hoare. Es decir,
vc C Q ⟹ ⊢ {pre C Q} strip C {Q}
*}
lemma vc_sound: "vc C Q ⟹ ⊢ {pre C Q} strip C {Q}"
proof(induction C arbitrary: Q)
case (Awhile I b C)
show ?case
proof(simp, rule While')
from `vc (Awhile I b C) Q`
have vc: "vc C I" and IQ: "∀s. I s ∧ ¬ bval b s ⟶ Q s" and
pre: "∀s. I s ∧ bval b s ⟶ pre C I s" by simp_all
have "⊢ {pre C I} strip C {I}" by(rule Awhile.IH[OF vc])
with pre show "⊢ {λs. I s ∧ bval b s} strip C {I}"
by(rule strengthen_pre)
show "∀s. I s ∧ ¬bval b s ⟶ Q s" by(rule IQ)
qed
qed (auto intro: hoare.conseq)
text{* Aplicando el reforzamiento de la precondición obtenemos
el siguiente corolario.
*}
corollary vc_sound':
"⟦ vc C Q; ∀s. P s ⟶ pre C Q s ⟧ ⟹ ⊢ {P} strip C {Q}"
by (metis strengthen_pre vc_sound) -- "usando Sledgehammer"
text{* A partir del resultado se puede considerar el siguiente
procedimiento para probar ⊢ {P} c{Q}:
(+) Anotar c con invariantes y obtener C tal que strip C = c.
(+) Probar la condición de verificación (vc C Q).
(+) Probar que P implica la precondición (pre C Q).
*}
text{* Completitud de pre y vc con respecto a ⊢:
⊢ {P}c{Q} ⟹ ∃C. strip C = c ∧ vc C Q ∧ (∀s. P s ⟶ pre C Q s)
*}
text{* Son necesarios los siguientes lemas previos.
*}
text{* Lema: monotonía de la función pre.
*}
lemma pre_mono:
"∀s. P s ⟶ P' s ⟹ pre C P s ⟹ pre C P' s"
proof (induction C arbitrary: P P' s)
case Aseq thus ?case by simp metis
qed simp_all
text{* Lema: monotonía de la función pre.
*}
lemma vc_mono:
"∀s. P s ⟶ P' s ⟹ vc C P ⟹ vc C P'"
proof(induction C arbitrary: P P')
case Aseq thus ?case by simp (metis pre_mono)
qed simp_all
theorem vc_complete:
"⊢ {P}c{Q} ⟹ ∃C. strip C = c ∧ vc C Q ∧ (∀s. P s ⟶ pre C Q s)"
(is "_ ⟹ ∃C. ?G P c Q C")
proof (induction rule: hoare.induct)
case Skip
show ?case (is "∃C. ?C C")
proof show "?C Askip" by simp qed
next
case (Assign P a x)
show ?case (is "∃C. ?C C")
proof show "?C(Aassign x a)" by simp qed
next
case (Seq P c1 Q c2 R)
from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast
from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast
show ?case (is "∃C. ?C C")
proof
show "?C(Aseq C1 C2)"
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
qed
next
case (If P b c1 Q c2)
from If.IH obtain C1 where ih1: "?G (λs. P s ∧ bval b s) c1 Q C1"
by blast
from If.IH obtain C2 where ih2: "?G (λs. P s ∧ ¬bval b s) c2 Q C2"
by blast
show ?case (is "∃C. ?C C")
proof
show "?C(Aif b C1 C2)" using ih1 ih2 by simp
qed
next
case (While P b c)
from While.IH obtain C where ih: "?G (λs. P s ∧ bval b s) c P C" by blast
show ?case (is "∃C. ?C C")
proof show "?C(Awhile P b C)" using ih by simp qed
next
case conseq thus ?case by(fast elim!: pre_mono vc_mono)
qed
end