Curso Doctorado: Métodos Formais para o desenvolvemento do Software
Bienio:1997-99, Curso:1998-99
 
 
 Semántica de un lenguaje imperativo simple
J. L. Freire
Seminario 4.1, 26 de Abril  a las 18 h.
 
 

El objetivo de esta lección es ilustrar con un ejemplo las funcionalidades del lenguaje de especificación Gallina asociado al cálculo de contrucciones inductivas (CCI) e implementado en el Sistema de Prueba Coq desarrollado en el INRIA.
 
El ejemplo elegido trata de la semántica de un mini-lenguaje de programación imperativo simple (sin tipos) del estilo de IMP ([22])
 

1  Introducción

Gallina es el nombre dado al lenguaje de especificación del sistema Coq (a Computer Aided Proof System). Permite definir: las definiciones que intervienen en la semántica de los lenguajes se representan particularmente bien en Gallina:

2  Presentación del problema

Nuestro lenguaje comprende los comandos siguientes, a partir de un conjunto de variables que denotaremos X :
                                    C ::=
  skip
| X:= a
| C1;C2
| if b then C1 else C2
| while b do C 
 
Figura 1: Sintáxis de los comandos
Las expresiones aritméticas se forman a partir de enteros:
a ::= 
 
X Variables
| n Constantes enteras
| a1 op a2 Operación binaria sobre los enteros
op ::= + | - | * | ..
 
 

Las expresiones booleanas se forman a partir de enteros y boleanos simples:

b ::= 
true |  false Constantes boleanas
| b1 xor b2 O exclusivo
| null b Test de nulidad de enteros
 
 Figura 2: Sintáxis de las expresiones
Se busca definir una semántica operacional para este lenguaje. Todas se representan en semántica natural por medio de la definición de una relación entre un programa y "valores"". Esta relación se describe con la ayuda de reglas de inferencia.

2.2  Semántica operacional

La semántica operacional define el programa como una transformación del estado de la memoria. Esta memoria la veremos como una función que asocia a cada variable, un valor que será una constante entera  n. Las dos operaciones sobre la memoria son la lectura y la actualización: si x es una variable, entonces m(x) representa el valor de la memoria para la variable  x, si v es un valor, entonces m[x¬ v] representa la memoria donde la variable x ha sido actualizada al valor v.  Así pues, se tendrá:
(m[x¬ v])(x) = v.

Semántica de las expresiones

Se necesita una relación que asocie a cada memoria  m y expresión E un valor v que represente el resultado de la evaluación de E en la memoria m. Se denota esta relación
m |- E |> v
que podemos leer "en el estado (o memoria) m la expresión E  tiene el valor v".
    Se utilizarán constantes y funciones sobre el dominio de valores, que realicen las operaciones concretas (boleanas o aritméticas). Las escribiremos en itálica utilizando el mismo identificador que en la sintáxis: así por ejemplo, a la construcción sintáctica xor le corresponderá la función semántica concreta xor .
 
m|- X |>m(X)
m|- true|> true
m|- false|> false
m|- n|> n
 
m|- E1|> b1   m|- E2|> b2
m|- E1 xor E2|> b1 xor  b2
m|- E|> n
m|- null E |> null  n 
m|- E1|> n1   m|- E2|> n2
m|- E1 op E2|> n1 op  n2
 
Figura 5: Semántica de las expresiones

Semántica de los comandos

La relación
m |- C |> m'
expresa que el comando C se ejecuta en un estado m que se transforma en otro  m'. Esta relación se define por las reglas de inferencia:
m |- skip |> m 
m|- E |> v
m |- X:= E |> m[X¬ v]
 		  
m|- C1 |> m1   m1|- C2 |> m'
m|- C1 ; C2 |> m'
 
 
m|- E |> true    m|- C1|> m'
m|- if E then C1 else C2 |> m'
 		  
m|- E |> false    m|- C2|> m'
m|- if E then C1 else C2 |> m'
 
 
m|- E |> true    m|- C|> m1    m1|-while E do C |> m' 
m|- while E do C |> m'
 		  
m|- E |> false 
m|- while E do C |> m
 
 
 
Figure 6: Semática de los comandos

 

3  Especificaciones en Gallina

Veamos ahora como se puede representar la teoría precedente en Gallina.

3.1  Las expresiones

Definiciones

Vamos a representar las variables y los operadores binarios por conjuntos paramétricos  que podrán instanciarse en una segunda etapa.  En cambio, las funciones boleanas se representan de manera concreta por un constructor de un tipo de datos.

Coq < Variable name : Set.
Variable name : Set.
Coq < Variable op : Set.
op is assumed
Coq < Inductive aexpr : Set :=
     Var   : name -> aexpr
   | Num   : nat  -> aexpr
   | Opn   : op -> aexpr -> aexpr -> aexpr.
aexpr_ind is defined
aexpr_rec is defined
aexpr_rect is defined
aexpr is defined

Coq < Inductive bexpr : Set :=
     Tr  : bexpr
   | Fa  : bexpr
   | Xor : bexpr -> bexpr -> bexpr
   | Null: aexpr -> bexpr.
bexpr_ind is defined
bexpr_rec is defined
bexpr_rect is defined
bexpr is defined

 
 

Interpretación de las funciones

Las funciones semánticas que corresponden a los operadores concretos pueden ser programadas explícitamente. En cambio, la semántica de las operaciones aritméticas (que se ven de manera paramétrica) debe pasarse como parámetro.


Coq < Definition boolxor : bool->bool->bool
    := [b1,b2]if b1 then if b2 then false else true else b2.
boolxor is defined

Coq < Eval Compute in (boolxor true false).
     = true
     : bool

Coq < Eval Compute in (boolxor true true).
     = false
     : bool

Coq <  Definition iszero : nat->bool
    := [n:nat]Cases n of O => true | (S n) => false end.
iszero is defined

Coq <   Variable semop : op->nat->nat->nat.
semop is assumed
 
 

Coq < Definition memory := name->nat.

Valor de una expresión

Para construir la relación entre una expresión y su valor, se puede dar una memoria como un parámetro en una ``Section'', cuando la sección se cierra, las nociones introducidas serán automáticamente abstraidas respecto a los parámetros de los que dependan.

Coq < Section Valexpr.

Coq < Variable memstate : memory.

 La definición aexprval formaliza la semántica de las expresiones aritméticas y bexprval las de las booleanas, tal y como se presentó en la figura  5.

Coq < Inductive aexprval : aexpr -> nat -> Prop :=
  valvar   : (x:name)
      (aexprval (Var x)(memstate x))
| valnum   : (n:nat)(aexprval (Num n) n)
| valopn   : (o:op)(f,g:aexpr)(nf,ng:nat)
     (aexprval f nf)->(aexprval g ng)
              ->(aexprval (Opn o f g)
                       (semop o  nf ng)).
aexprval_ind is defined
aexprval is defined

Inductive bexprval : bexpr -> bool -> Prop :=
  valtr    : (bexprval Tr true)
| valfa    : (bexprval Fa false)
| valxor   : (f,g:bexpr)(bf,bg:bool)
   (bexprval f bf)->(bexprval g bg)
  ->(bexprval (Xor f g) (boolxor bf bg))
| valtzero : (f:aexpr)(nf:nat)
(aexprval f nf)
   ->(bexprval (Null f) (iszero nf)).

Hint valvar valtr valfa valxor valnum valtzero valopn.

End Valexpr.
 

3.3  Los comandos

La representación de la sintáxis de los comandos, sigue las definiciones de la figura  1.
 
 

Sintáxis

Inductive com : Set :=
   skip  : com
 | aff   : name -> aexpr -> com
 | seq   : com  -> com  -> com
 | cond  : bexpr -> com  -> com -> com
 | while : bexpr -> com  -> com.
 

Comenzamos por declarar el axioma de decidibilidad de la igualdad sobre los nombres

Variable eq_name_dec : (x,y:name){x=y}+{~x=y}.

Podemos definir ahora la operación  update de actualización de la memoria que se hará en una sección introduciendo el nombre de la variable  y, el valor que le queremos asignar v y la memoria  m.

Section Update.
Variable y : name.
Variable v : nat.
Variable mem : memory.

Definition Ifdec : (A,B:Prop)({A}+{B})->nat->nat->nat
   := [A,B,H,p,q]if H then [_]p else [_]q.

Definition update : memory
  := [x:name]
    (Ifdec (eq_name_dec y x) v (mem x)).

Coq <Theorem update_eq : v = (update y).

La formulación, fuera de esta sección, sería:
update_eq :(y:name)(v:nat)(mem:memory)
                  v=(update y v mem y)
Unfold update.
Case (eq_name_dec y y).
Simpl.
Intro.
Trivial.

Simpl.
Intro.
Absurd y=y.
Trivial.

Trivial.
Save.
 

End Update.

Inductive semcom: memory->com->memory->Prop:=
  semskip: (m:memory)(semcom m skip m)
 |semaff:(m:memory)(n:name)(v:nat)(e:aexpr)
  (aexprval m e v)->
      (semcom m (aff n e) (update n v m))
 |semseq : (m1,m2,m3:memory)(c,d:com)
            (semcom m1 c m2)
              ->(semcom m2 d m3)
                ->(semcom m1 (seq c d) m3)
 |semcondtr:(m1,m2:memory)(e:bexpr)(c,d:com)
    (bexprval m1 e true)
       ->(semcom m1 c m2)
        ->(semcom m1 (cond e c d) m2)
 |semcondfa:(m1,m2:memory)(e:bexpr)(c,d:com)
      (bexprval m1 e false)
          ->(semcom m1 d m2)
            ->(semcom m1 (cond e c d) m2)
 |semwhiletr:(m1,m2:memory)(e:bexpr)(c:com)
     (bexprval m1 e true)
       ->(m3:memory)(semcom m1 c m3)
        ->(semcom m3 (while e c) m2)
         ->(semcom m1 (while e c) m2)
 |semwhilefa:(m:memory)(e:bexpr)(c:com)
      (bexprval m e false)
       ->(semcom m (while e c) m).

Hint semskip semseq semaff semcondtr semcondfa semwhiletr semwhilefa.

Lemma ejemplo1:(m,m':memory)(b:bexpr)(c:com)
(semcom m (while b c) m')->
     (semcom m (cond b (seq
                            c
                            (while b c))
                            skip)
                     m').

Intros.Inversion H;Intros;EAuto.
Save.

Lemma ejemplo2:(m,m':memory)(b:bexpr)(c:com)
(semcom m (cond b (seq  c  (while b c))  skip)  m') -> (semcom m (while b c) m').

Intros.
Inversion H.
(Inversion H6; EAuto).

Inversion H6.
Rewrite <- H9.
Auto.
 

Bibliografía

[1]
 Y. Bertot. A certified compiler for an imperative language. Rapport de Recherche RR-34-88, INRIA, 1998.
[2]
 C. Böhm and A. Berarducci. Automatic synthesis of typed l-programs on term algebras. Theoretical Computer Science, 39, 1985.
[3]
 D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn. A simple applicative language: Mini-ml. Rapport de Recherche 529, INRIA, Mai 1986.
[4]
 Th. Coquand. An analysis of girard's paradox. In Symposium on Logic in Computer Science, Cambridge, MA, 1986. IEEE Computer Society Press.
[5]
 Th. Coquand. Metamathematical investigations of a Calculus of Constructions. In P. Oddifredi, editor, Logic and Computer Science. Academic Press, 1990. Rapport de recherche INRIA 1088, also in [8].
[6]
 Th. Coquand. Pattern matching with dependent types. In Nordström et al. [15].
[7]
 Th. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, volume 806 of Lecture Notex in Computer Science, pages 62--78. Springer-Verlag, 1994.
[8]
 G. Huet ed. The Calculus of Constructions, Documentation and user's guide, Version V4.10, 1989. Rapport technique INRIA 110.
[9]
 E. Giménez. A tutorial on recursive types in coq, Mars 1996. Notes de cours rédigées pour la formation Coq, http://pauillac.inria.fr/ gimenez.
[10]
 J.-Y. Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la téorie des types. In Proceedings of the 2nd Scandinavian Logic Symposium. North-Holland, 1970.
[11]
 J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972.
[12]
 J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
[13]
 K. Gödel. Über einer bisher noch nicht benützte erweiterung des finiten standpunktes. Dialectica, 12, 1958. Traduit dans le Journal of Philosophical Logic 9, 1980. Réedité avec traduction anglaise dans les oeuvres complètes.
[14]
 Th. Kleymann. Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, Edinburgh-LFCS-Technical Report ECS-LFCS-98-392, 1998.
[15]
 B. Nordström, K. Petersson, and G. Plotkin, editors. Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992.
[16]
 P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984.
[17]
 C. Paulin-Mohring. Extracting Fw's programs from proofs in the Calculus of Constructions. In Association for Computing Machinery, editor, Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989.
[18]
 C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Université Paris 7, January 1989.
[19]
 F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Proceedings of Mathematical Foundations of Programming Semantics, LNCS 442. Springer-Verlag, 1990. also technical report CMU-CS-89-209.
[20]
 Th. Schreiber. Auxiliary variables and recursive procedures. In TAPSOFT'97, volume 1214 of LNCS, pages 697--711, 1997.
[21]
 B. Werner. A normalization proof for an impredicative type system with large elimination over integers. In Nordström et al. [15].
[22]
 G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.
 

Ayudas

Inversion  Let the type of ident  in the local context be (I vec(t)), where I is a (co)inductive predicate. Then, Inversion applied to ident  derives for each possible constructor ci of (I vec(t)), all the necessary conditions that should hold for the instance (I vec(t)) to be proved by ci.

Por ejemplo, dado el predicado inductivo  semcom: memory->com->memory->Prop con constructores:
   semskip     : (m:memory)(semcom m skip m)
 | semaff : (m:memory)(n:name)(v:nat)(e:aexpr)
        (aexprval m e v)->(semcom m (aff n e) (update n v m))
 | semseq : (m1,m2,m3:memory)(c,d:com)
                (semcom m1 c m2)
                  ->(semcom m2 d m3)
                    ->(semcom m1 (seq c d) m3)
 |semcondtr:(m1,m2:memory)(e:bexpr)(c,d:com)
         (bexprval m1 e true)
            ->(semcom m1 c m2)
              ->(semcom m1 (cond e c d) m2)
 |semcondfa:(m1,m2:memory)(e:bexpr)(c,d:com)
      (bexprval m1 e false)
          ->(semcom m1 d m2)
            ->(semcom m1 (cond e c d) m2)
 |semwhiletr:(m1,m2:memory)(e:bexpr)(c:com)
     (bexprval m1 e true)
       ->(m3:memory)(semcom m1 c m3)
        ->(semcom m3 (while e c) m2)
         ->(semcom m1 (while e c) m2)
 |semwhilefa:(m:memory)(e:bexpr)(c:com)
      (bexprval m e false)
       ->(semcom m (while e c) m).
si tenemos en el entorno un identificador H que tiene como tipo
(semcom m (while b c) m'), es decir, el predicado inductivo aplicado a un determinado vector de valores (m, (while b c), m'), entonces, la táctica Inversion H para cada constructor va unificando ls expresión (semcom m (while b c) m')con los "finales" de los tipos de los constructores y obteniendo como hipótesis sustitutorias de H (para cada unificación con éxito se obtiene un subgoal y unas hipótesis sustitutorias) las "premisas" correspondientes. Así, en este caso, en el constructor semwhilefa la unificación de (semcom m (while b c) m')<->(semcom m (while e c) m) da origen a {b=c, m'=m, (bexprval m b false)}.En semwhiletr la unificación de (semcom m (while b c) m')<->(semcom m1 (while e c) m2) da origen a {m=m1, e=b, m'=m2, (semcom m3 (while b c) m'),(m3:memory)(semcom m c m3), (bexprval m e true)}
y obtendremos por lo tanto dos subgoals  (semcom m' (cond b (seq c (while b c)) skip) m') y  (semcom m (cond b (seq c (while b c)) skip) m')
 
  Resumen de este primer ejemplo

 
 Otro ejemplo (del Tutorial),