Curso Doctorado: Métodos Formais para o desenvolvemento do Software
Bienio:1997-99, Curso:1998-99
 

 Semántica axiomática de un lenguaje imperativo simple
J. L. Freire
Seminario 4.1, 3 de Mayo a las 18 h.
 

Semántica axiomática

Se trata de interpretar los comandos como transformaciones de predicados que especifican propiedades de la memoria o estado. Si P y Q son dos de tales predicados y C es un comando, entonces se define la proposición {P}C{Q} con el objetivo de que represente la siguiente interpretación: la ejecución de C a partir de una memoria que satisface P conduce a una memoria que satisface Q.

La conjunción y la implicación de dos predicados se escribirán P Ù Q y P Þ Q, si x es una variable y E una expresión, entonces  P[x¬ E] representa el predicado que a cualquier memoria  m le asocia P(m[x¬ v]) donde v es el valor tal que m |- E |> v. Si w es un valor, entonces E=w representa el predicado que a todo m le asocia la propiedad v=w donde v es el valor tal que m |- E |> v.

La definición de esta relación está dada por las reglas de inferencia de la figura 1


{P}skip{P}     {P[X¬ E]}X := E{P} 
{P}C1{P1}   {P1}C2{Q}
{P}C1 ; C2{Q}
 
 
{P Ù (E=true )}C1{Q}
{P}if E then C1 else C2{Q}
 		  
{P Ù (E=false )}C2{Q}
{P}if E then C1 else C2{Q}
 
 
{P Ù (E=true )}C{P}
{P}while E do C{ P Ù (E=false )}
 
 
P Þ P1    {P1}C{Q1}  Q1Þ Q
{P}C{Q}
 
 

Figura 1: Semántica axiomática de los comandos

Una aserción es una propiedad de la memoria, representada por un predicado unario. En lógica de Hoare, este predicado unario se define concretamente por una fórmula lógica utilizando las variables del programa para representar los valores correspondientes de la memoria.

Coq < Definition Assertion := memory->Prop.
 

Transformaciones de predicados

Son las operaciones usuales de la lógica y de las transformaciones de aserciones.

Coq < Definition Istrue : bexpr->Assertion
 := [E:bexpr][m:memory](bexprval m E true).

Coq < Definition Isfalse : bexpr->Assertion
 := [E:bexpr][m:memory](bexprval m E false).

Coq < Inductive AndAss [P,Q:Assertion;m:memory] : Prop :=  Conjass : (P m)->(Q m)->(AndAss P Q m).

Hint Conjass.

Coq < Definition ImplAss : Assertion->Assertion->Prop
 :=  [P,Q:Assertion](m:memory)(P m)->(Q m).

El transformador siguiente corresponde a lo que sa ha denotado P[X¬ E]. El término  (memupdate x E P) representa el predicado que en un estado m vale P(m[X¬ v]), siendo v el valor de la expresión  E en la memoria m.

Coq < Definition memupdate : name->expr->Assertion->Assertion :=
  [x:name][e:expr][P:Assertion][m:memory]
 (v:semval)(exprval m e v)->(P (update x v m)).

es decir, (P[x¬ e]) m := P(m([x¬ v])) si  m |- e |> v.

Definición de {P}C{Q}

Se define el predicado (trueform P c Q) que corresponde con la definición de  {P}C{Q} tal y como se describió en la figura  1.

Coq < Inductive trueform : Assertion->com->Assertion->Prop
 := trueskip: (P:Assertion)(trueform P skip P)
 | trueaff : (P:Assertion)(n:name)(e:expr)
        (trueform (memupdate n e P) (aff n e) P)
 | trueseq : (P,Q,R:Assertion)(c,d:com)
          (trueform P c R)->(trueform R d Q)
             ->(trueform P (seq c d) Q)
 | truecond: (P,Q:Assertion)(e:expr)(c,d:com)
          (trueform (AndAss P (Istrue e)) c Q)
            ->(trueform (AndAss P (Isfalse e)) d Q)
               ->(trueform P (cond e c d) Q)
 | truewhile: (P:Assertion)(e:expr)(c:com)
    (trueform (AndAss P (Istrue e)) c P)
     ->(trueform  P (while e c) (AndAss P (Isfalse e)))
 | truecons : (P,P1,Q,Q1:Assertion)(c:com)
        (ImplAss P P1)->(trueform P1 c Q1)->(ImplAss Q1 Q)
               ->(trueform P c Q).
 

Lema de corrección

El siguiente teorema establece la corrección de la relación dada  {P}C{Q} respecto a la semántica.

Coq < Theorem truecorrect:
    (P,Q:Assertion)(c:com)
          (trueform P c Q)->(m1,m2:memory)
               (semcom m1 c m2)->(P m1)->(Q m2).

La demostración, requiere algunas construcciones intermedias.

Definition ifProp : bool -> Prop -> Prop -> Prop
 := [b,A,B]if b then A else B.

Local semcom_prop := [m,m':memory][c:com]
  Cases c of
  skip          =>  m=m'
| (aff n e)     =>  (EX v:nat | (aexprval m e v) & (update n v m)=m')
| (seq c1 c2)   =>
        (EX m1:memory | (semcom m c1 m1) & (semcom m1 c2 m'))
| (cond e c1 c2)=>
        (EX b:bool | (bexprval m e b) &
             (ifProp b (semcom m c1 m') (semcom m c2 m')))
| (while e c1)  =>
        (EX b:bool | (bexprval m e b) &
  (ifProp b  (EX m1:memory |(semcom m c1 m1)&
                           (semcom m1 (while e c1) m'))
             m=m'))
end.

Lemma semcom_inv :
        (m1,m2:memory)(c:com)(semcom m1 c m2)->(semcom_prop m1 m2 c).
Goal.
Induction 1; Simpl.
Trivial.
Intros; Exists v; Auto.
Intros; Exists m3; Auto.
Intros; Exists true; Trivial.
Intros; Exists false; Trivial.
Intros; Exists true; Simpl; Auto.
Exists m4; Auto.
Intros; Exists false; Simpl; Auto.
Save.

Goal.
Induction 1; Intros.
Elim (semcom_inv m1 m2 skip); Auto.
Elim (semcom_inv m1 m2 (aff n e)); Trivial.
Destruct 2; Apply H1; Trivial.
Elim (semcom_inv m1 m2 (seq c0 d)); Trivial.
Intros; Apply (H3 x m2); Trivial.
Apply (H1 m1 x); Auto.
Elim (semcom_inv m1 m2 (cond e c0 d)); Trivial.
Destruct x; Simpl; Intros.
Apply (H1 m1); Auto.
Apply (H3 m1); Auto.

 Local AndAsswhile :=
   [c:com][m,m':memory][P0:Assertion]
   Cases c of
    skip           => True
  | (aff n e)      => True
  | (seq c1 c2)    => True
  | (cond e c1 c2) => True
  | (while e c1)   => ((m1,m2:memory)
        (semcom m1 c1 m2)->(AndAss P0 (Istrue e) m1)->(P0 m2))
              ->(P0 m)->(AndAss P0 (Isfalse e) m')
   end.
Generalize H1 H3.
Change (AndAsswhile (while e c0) m1 m2 P0).
Elim H2; Simpl; Auto.
Intros.
Apply H8; Trivial.
Apply (H9 m0); Auto.

Apply (H3 m2); Apply (H2 m1); Trivial.
Apply (H0 m1); Trivial.
Save.