Curso Doctorado: Métodos Formais para o desenvolvemento do Software
Bienio:1997-99, Curso:1998-99
José L. Freire Nistal
J. M. Barja Pérez

Semántica de un lenguaje J. L. Freire Seminario 4.1, Lunes 15 de Marzo a las 18 h.

Basado en un ejemplo del curso: Calcul des Constructions Inductives Christine Paulin-Mohring et Benjamin Werner 1999

Semántica de un mini-lenguaje

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 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 (tipado, evaluación y semántica axiomática). Se proponen varias soluciones a la modelización de las diferentes nociones presentadas.

1 Introducción

Gallina es el nombre dado al lenguaje de especificación del sistema Coq (a Computer Aided Proof System). Permite definir:

tipos de datos estructurados,
funciones que pueden ser recursivas sobre la estructura de los datos,
relaciones especificadas inductivamente por un conjunto de propiedades de clausura,
fórmulas del cálculo de predicados de orden superior.

las definiciones que intervienen en la semántica de los lenguajes se representan particularmente bien en Gallina:

los árboles de sintáxis abstracta se codifican de modo natural como tipos de datos estructurados,
el orden superior permitirá manipular fácilmente los estados (memorias) que podrán verse como funciones, así como las aserciones que serán predicados sobre los estados o memorias,
las definiciones semánticas tales como el tipado o la evaluación, cuando se presentan como un conjunto de reglas de inferencia, se traducen inmediatamente a definiciones inductivas.

2 Presentación del problema

Nuestro lenguaje comprende los comandos siguientes, a partir de un conjunto de variables que denotaremos X :

C ::=

skip

| X:= E

| C₁;C₂

| if E then C₁ else C₂

| while E do C

Figura 1: Sintáxis de los comandos

Las expresiones se forman a partir de enteros y boleanos simples con la sintáxis de la figura 2.

E ::=

X^s Variables tipadas

| true | false Constantes boleanas

| E₁ xor E₂ O exclusivo

| n Constantes enteras

| null E Test de nulidad de enteros

| E₁ op E₂ Operación binaria sobre los enteros

s ::= nat | bool

op ::= + | - | * | ...

Figura 2: Sintáxis de las expresiones

Se busca definir semánticas estáticas, operacionales naturales y axiomáticas 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.1 Semántica estática

Se trata de determinar de manera estática (sin ejecutarlo) que un programa está bien formado. Es preciso, por lo tanto, verificar que en las expresiones condicionales o de bucle, los tests se hacen sobre expresiones booleanas. Esto implica definir una relación de tipado sobre las expresiones. Los valores posibles serán de los dos tipos básicos nat y bool.

La relación de tipado E:s se define por los axiomas y reglas de la figura 3.

X^s:s     true:bool     false:bool     n:nat

E₁:bool   E₂:bool

E₁ xor E₂:bool

E:nat

null E:bool

E₁:nat   E₂:nat

E₁ op E₂:nat

Figura 3: Semántica estática de las expresiones

Para los comandos, se define la relación C: ok por las reglas de la figura 4.

skip: ok

E:s

X:= E: ok

C₁: ok C₂ : ok

C₁;C₂: ok

E:bool C₁: ok C₂: ok

if E then C₁ else C₂: ok

E:bool C: ok

while E do C:ok

Figura 4: Semántica estática de los comandos

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 par formado por una variable y su tipo, un valor que será una constante entera n o boleana b. Las dos operaciones sobre la memoria son la lectura y la actualización: si x es una variable y s un tipo, entonces m(x,s) representa el valor de la memoria para la variable x y el tipo s, si v es un valor, entonces m[x¬ v] representa la memoria donde la variable x ha sido actualizada al valor v. El tipo de la variable afectada no figura aquí explicitamente pero puede deducirse del tipo del valor v. Así pues (m[x¬ v])(x,s) = 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 m la expresión E tiene el valor v".
Se utilizarán constantes y funciones sobre el dominio de valores, que realicen las operaciones boleanas o artiméticas y 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 xor .

m|- X^s|>m(X,s)     m|- true|> true       m|- false|> false      m|- n|> n

m|- E₁|> b₁   m|- E₂|> b₂

m|- E₁ xor E₂|> b₁ xor b₂

m|- E|> n

m|- null E |> null n

m|- E₁|> n₁   m|- E₂|> n₂

m|- E₁ op E₂|> n₁ op n₂

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 de la figura 6.

m |- skip |> m

m|- E |> v

m |- X:= E |> m[X¬ v]

m|- C₁ |> m₁   m₁|- C₂ |> m'

m|- C₁ ; C₂ |> m'

m|- E |> true    m|- C₁|> m'

m|- if E then C₁ else C₂ |> m'

m|- E |> false    m|- C₂|> m'

m|- if E then C₁ else C₂ |> m'

m|- E |> true    m|- C|> m₁    m₁|-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

2.3 Semántica axiomática

Se trata de interpretar los comandos como transformaciones de predicados que especifican propiedades de la memoria o estado. Si P yQ son dos de tales predicados y C es un comando, entonces se define {P}C{Q} con 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 7.

{P}skip{P}     {P[X¬ E]}X := E{P}

{P}C₁{P₁}   {P₁}C₂{Q}

{P}C₁ ; C₂{Q}

{P Ù (E=true )}C₁{Q}

{P}if E then C₁ else C₂{Q}

{P Ù (E=false )}C₂{Q}

{P}if E then C₁ else C₂{Q}

{P Ù (E=true )}C{P}

{P}while E do C{ P Ù (E=false )}

P Þ P₁    {P₁}C{Q₁}   Q₁Þ Q

{P}C{Q}

Figure 7: Semántica axiomática de los comandos

2.4 Propiedades a demostrar

Entre las propiedades que interesa demostrar están:

Decibilidad de la corrección respecto a la semántica estática (algoritmo de tipado).
Que toda expresión correctamente tipada admite un valor.
Corrección de la semántica axiomática. Es decir, si {P}C{Q} se verifica, entonces toda evaluación de C en una memoria que verifique P conduce a una memoria que verifica Q.

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. Esta elección permite ilustrar dos tratamientos posibles de los operadores del lenguaje que se trata de modelar.

Coq < Variable name : Set.

Coq < Inductive sort : Set := Sbool : sort | Snat : sort.

Coq < Variable op : Set.

Expresiones correctas

El predicado exprcorrect traduce la relación descrita en la figura 3. Cada regla de inferencia que define la relación se traduce en un constructor de la definición inductiva. Las variables libres de las definiciones aparecerán como variables cuantificadas universalmente en los constructores.

Coq < Inductive exprcorrect : sort -> expr -> Prop
Coq <   := corvar   : (n:name)(s:sort)(exprcorrect s (Var n s))
Coq <   | cortr    : (exprcorrect Sbool Tr)
Coq <   | corfa    : (exprcorrect Sbool Fa)
Coq <   | corxor   : (b,c:expr)(exprcorrect Sbool b)->(exprcorrect Sbool c)
Coq <                ->(exprcorrect Sbool (Xor b c))
Coq <   | cornum   : (n:nat)(exprcorrect Snat (Num n))
Coq <   | cornull : (e:expr)(exprcorrect Snat e)->(exprcorrect Sbool (Null e))
Coq <   | corop    : (o:op)(e,f:expr)(exprcorrect Snat e)->(exprcorrect Snat f)
Coq <               ->(exprcorrect Snat (Opn o e f)).

Dominios Semánticos

Se trata de representar el dominio semántico de las variables. A cada tipo de variable le corresponde un conjunto en el sentido matemático, que se representa mediante un tipo de dato Coq, aquí, el tipo de los boleanos o de los enteros. El dominio semántico de los valores semval se representa por la suma disjunta de los dos tipos.

Coq < Inductive semval : Set :=
Coq < Bool : bool -> semval
Coq < | Nat : nat -> semval.

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
Coq < := [b1,b2]if b1 then if b2 then false else true else b2.

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

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

Compatibilidad entre tipos y valores

Deberemos ligar la clase de las expresiones y el tipo de su interpretación semántica. Para ello, se define sort_val que es una función de los dominios semánticos en las clases, que a cada valor semántico le asocia la clase correspondiente.

Coq < Definition sort_val : semval -> sort
Coq < := [v:semval]Cases v of (Bool b)=>Sbool | (Nat n)=>Snat end.

Se utilizará igualmente una relación compat entre los valores y las clases, tal que (compat Sbool v) sea equivalente a $ b:bool.v=(Bool b) (definida por el predicado valbool) y (compat Snat v) equivalente a $ n:nat.v=(Nat n) (definida por el predicado valnat).

Coq < Inductive valbool : semval->Prop
Coq < := valbool_intro : (b:bool)(valbool (Bool b)).

Coq < Inductive valnat : semval->Prop
Coq < := valnat_intro : (n:nat)(valnat (Nat n)).

Coq < Definition compat : sort -> semval -> Prop
Coq < := [s,v]Cases s of Sbool => (valbool v) | Snat => (valnat v) end.

Nótese que la definición inductiva de valbool es una codificación inductiva directa del predicado [x:semval](EX b:bool | x=(Bool b)). Se puede probar fácilmente la correspondencia entre compat y sort_val.

Coq < Theorem compat_sort_val
Coq < : (s:sort)(v:semval)(compat s v)->s=(sort_val v).

Una alternativa podría ser la de representar la noción de compatibilidad por un predicado inductivo:

Coq < Inductive compat1 : sort -> semval -> Prop :=
Coq < compat_bool : (b:bool)(compat1 Sbool (Bool b))
Coq < | compat_nat : (n:nat)(compat1 Snat (Nat n)).

Las dos definiciones son equivalentes. Nótese que en el segundo caso, la propiedad

(compat1 Snat v) ® $ n : nat v=(Nat n) necesita una inversión del predicado inductivo, mientras que en el caso de compat esto es una simple consecuencia del cálculo de la expresión Cases y de la definición de valnat.

La memoria

La memoria se representa como una función que a toda variable y clase le asocia un valor semántico. Será pues neccesario suponer que este valor es compatible con la clase

Coq < Definition memory := name->sort->semval.

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.

Coq < Hypothesis memstate_correct : (n:name)(s:sort)(compat s (memstate n s)).

La definición exprval formaliza la semántica de las expresiones tal como se presentó en la figura 5.

Coq < Inductive exprval : expr -> semval -> Prop :=
Coq <   valvar   : (n:name)(s:sort)(exprval (Var n s) (memstate n s))
Coq < | valtr    : (exprval Tr (Bool true))
Coq < | valfa    : (exprval Fa (Bool false))
Coq < | valxor   : (f,g:expr)(bf,bg:bool)
Coq <              (exprval f (Bool bf))->(exprval g (Bool bg))
Coq <               ->(exprval (Xor f g) (Bool (boolxor bf bg)))
Coq < | valnum   : (n:nat)(exprval (Num n) (Nat n))
Coq < | valtzero : (f:expr)(nf:nat)(exprval f (Nat nf))
Coq <               ->(exprval (Null f) (Bool (iszero nf)))
Coq < | valopn   : (o:op)(f,g:expr)(nf,ng:nat)
Coq <              (exprval f (Nat nf))->(exprval g (Nat ng))
Coq <               ->(exprval (Opn o f g) (Nat (semop o nf ng))).

Ahora se puede enunciar el teorema que nos asegura que toda expresión correctamente tipada admite un valor.

Coq < Theorem expr_val_cor :
Coq < (E:expr)(s:sort)(exprcorrect s E)->(EX v:semval | (exprval E v)).

La demostración por recurrencia necesita un lema más fuerte que diga que el valor calculado es compatible con la clase de la expresión.

Coq < Lemma expr_val_cor_dom :
Coq < (E:expr)(s:sort)(exprcorrect s E)
Coq < ->(EX v:semval | (compat s v) & (exprval E v)).

Representación de la memoria con tipos dependientes

El tratamiento de la relación entre la clase de la expresión y el dominio del valor semántico es pesada. Se puede utilizar la expresividad del lenguaje de especificación de Coq para utilizar otros formalismos. Se construye una familia dependiente sval (cuyo tipo es sort® Set) que a la clase Sbool le asocie el tipo bool y a Snat le asocie el tipo nat. El dominio semántico semval podría representarse por un par formado por una clase s y un objeto de tipo (sval s), lo cual es simplemente codificar una suma disjunta explícitamente por medio de la utilización de un selector s y de un campo cuyo tipo varía según el selector.

Se puede simplificar la representación haciendo implícita en la definición de la memoria la noción de compatibilidad.

Coq < Definition sval : sort -> Set
Coq < := [s]Cases s of Sbool => bool | Snat => nat end.

Coq < Definition memory1 := name->(s:sort)(sval s).

Se define entonces:

Coq < Variable memstate1 : memory1.

Coq < Inductive exprval1 : expr -> (s:sort)(sval s) -> Prop :=
Coq <   valvar1   : (n:name)(s:sort)(exprval1 (Var n s) s (memstate1 n s))
Coq < | valtr1    : (exprval1 Tr Sbool true)
Coq < | valfa1    : (exprval1 Fa Sbool false)
Coq < | valxor1   : (f,g:expr)(bf,bg:bool)
Coq <              (exprval1 f Sbool bf)->(exprval1 g Sbool bg)
Coq <               ->(exprval1 (Xor f g) Sbool (boolxor bf bg))
Coq < | valnum1   : (n:nat)(exprval1 (Num n) Snat n)
Coq < | valtzero1 : (f:expr)(nf:nat)(exprval1 f Snat nf)
Coq <               ->(exprval1 (Null f) Sbool (iszero nf))
Coq < | valopn1   : (o:op)(f,g:expr)(nf,ng:nat)
Coq <              (exprval1 f Snat nf)->(exprval1 g Snat ng)
Coq <               ->(exprval1 (Opn o f g) Snat (semop o nf ng)).

El lema de corrección de la evaluación se enuncia entonces simplemente:

Coq < Theorem expr_val_cor1 :
Coq < (E:expr)(s:sort)(exprcorrect s E)->(EX v:(sval s) | (exprval1 E s v)).

La formalización y la prueba son así más simples, sin embargo, el uso de los tipos dependientes hace que la formalización de la función de escritura sobre la memoria sean más complicada. En efecto, se debe tener con n:name,s:sort,v:(sval s),mem:memory1

Coq < Definition update : (m:nat)(s':sort)(sval s').

El simple hecho de saber que s=s' no basta para asegurar que el término v de tipo (sval s) es también de tipo (sval s'). Será necesario utilizar un análisis por casos según los valores de s y s'. Este análisis no hubiera sido posible si el conjunto de clases hubiera permanecido paramétrico.

De forma general, en presencia de los tipos dependientes, el uso de la igualdad es delicado. No es posible, por ejemplo, escribir v=v' con v:(sval s) y v':(sval s') salvo cuando s y s' sean convertibles. La presencia de una hipótesis s=s' es insuficiente. Será preciso utilizar nociones más complejas de igualdad.

3.2 Verificación del tipo y evaluación constructiva

Se podría definir el hecho de que una expresión e está mal formada como la propiedad: " s:sort.¬ (exprcorrect s e) Pero resulta más fácil manejar definiciones positivas dando una noción constructiva de espresión errónea enumerando los casos posibles de fallo. Ello provee de una interpretación constructiva de la prueba de que una expresión es errónea lo cual permitirá encontrar exactamente la naturaleza del error al saber en qué subtérmino se ha aplicado un operador a una expresión de una clase no adecuada.

Coq < Inductive exprerr : expr -> Prop
Coq <   := errxorl     : (b,c:expr)(exprcorrect Snat b)->(exprerr (Xor b c))
Coq <   | errxorr      : (b,c:expr)(exprcorrect Snat c)->(exprerr (Xor b c))
Coq <   | errtzero     : (b:expr)(exprcorrect Sbool b)->(exprerr (Null b))
Coq <   | erropl       : (op:op)(b,c:expr)
Coq <                    (exprcorrect Sbool b)->(exprerr (Opn op b c))
Coq <   | erropr       : (op:op)(b,c:expr)
Coq <                    (exprcorrect Sbool c)->(exprerr (Opn op b c))
Coq <   | errcongxorl : (b,c:expr)(exprerr b)->(exprerr (Xor b c))
Coq <   | errcongxorr : (b,c:expr)(exprerr c)->(exprerr (Xor b c))
Coq <   | errcongtzero : (b:expr)(exprerr b)->(exprerr (Null b))
Coq <   | errcongopl   : (op:op)(b,c:expr)(exprerr b)->(exprerr (Opn op b c))
Coq <   | errcongopr   : (op:op)(b,c:expr)(exprerr c)->(exprerr (Opn op b c)).

El teorema que expresa la decidibilidad del tipado y la evaluación es justamente una prueba del hecho de que para toda expresión E, o bien es posible construir un valor v de la expresión cuyo tipo es el de la expresión, o bien se puede probar que la expresión E está mal formada. El hecho de utilizar una noción constructiva de la disyunción y del existencial, asegura la existencia de un algoritmo que permita decidir en qué caso estamos y calcular efectivamente el valor. Se establece así un resultado de decibilidad sin tener que representar una noción de computabilidad.

Coq < Theorem expr_val_check_proof :
Coq < (E:expr){v:semval | (exprval E v) & (exprcorrect (sort_val v) E)}
Coq < +{exprerr E}.

Si nos centramos solamente en la parte de cálculo de esta prueba, se tendrá una función eval_prog que a toda expresión le asocia un valor o nada en absoluto. Esta función puede representarse igualmente en Gallina utilizando el tipo Exc de Coq análogo al tipo option de CAML.

Coq < Print Exc.
Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)

La función eval_prog se calcula mediante un punto fijo estructural sobre la expresión.

Coq < Fixpoint eval_prog [e:expr]:(Exc semval)
Coq < := Cases e of
Coq <    (Var n s) => (value semval (memstate n s))
Coq <   | Tr       => (value semval (Bool true))
Coq <   | Fa       => (value semval (Bool false))
Coq <   |(Xor f g) => Cases (eval_prog f) (eval_prog g) of
Coq <                  (value (Bool bf)) (value (Bool bg)) =>
Coq <                                 (value semval (Bool (boolxor bf bg)))
Coq <                 | _               _              => (error semval)
Coq <                 end
Coq <   |(Num n)   => (value semval (Nat n))
Coq <   |(Null f) => Cases (eval_prog f) of
Coq <                  (value (Nat nf)) => (value semval (Bool (iszero nf)))
Coq <                 | _               => (error semval)
Coq <                 end
Coq <   |(Opn o f g) => Cases (eval_prog f) (eval_prog g) of
Coq <                  (value (Nat nf)) (value (Nat ng)) =>
Coq <                                 (value semval (Nat (semop o nf ng)))
Coq <                 | _               _            => (error semval)
Coq <                 end
Coq <   end.

Coq < End Valexpr.

3.3 Los comandos

La representación de la sintáxis y de la semántica estática de los comandos, sigue las definiciones de las figuras 1 y 4.

Sintáxis

Coq < Inductive com : Set :=
Coq <    skip : com
Coq < | aff   : name -> expr -> com
Coq < | seq   : com -> com -> com
Coq < | cond : expr -> com -> com -> com
Coq < | while : expr -> com -> com.

Semántica estática

Coq < Inductive comcorrect : com->Prop
Coq <   := corskip : (comcorrect skip)
Coq <   | coraff : (n:name)(e:expr)(s:sort)(exprcorrect s e)
Coq <                 ->(comcorrect (aff n e))
Coq <   | corseq : (c,d:com)(comcorrect c)->(comcorrect d)->(comcorrect (seq c d))
Coq <   | corcond : (b:expr)(c,d:com)(exprcorrect Sbool b)
Coq <                 ->(comcorrect c)->(comcorrect d)->(comcorrect (cond b c d))
Coq <   | corwhile : (b:expr)(c:com)(exprcorrect Sbool b)->(comcorrect c)
Coq <                 ->(comcorrect (while b c)).

3.4 Actualización de la memoria

Definimos ahora la función de escritura en la memoria. Utilizaremos la decidibilidad de la igualdad sobre las variables, que viene de la decidibilidad de la igualdad sobre los nombres (tomada como axioma ya que el conjunto de los nombres no está especificado) y de la correspondiente sobre las clases que puede construirse explícitamente.
Para mostrar la decidibilidad de la igualdad sobre un conjunto A, se puede construir una función boleana f de tipoA ® A ® bool y demostrar que es la función característica de la igualdad (f x y)=true Û x=y. Elegimos aquí otra solución que consiste en construir un término fdec de tipo (x,y:A){x=y}+{¬(x=y)} que a cada x e y les asocia bien un objeto (left h) con h una prueba de x=y o bien un objeto (right h) con h una prueba de ¬(x=y).
Una expresión `` if a=b then p else q'' se escribirá en Coq:

Cases (fdec a b) of (left _) => p | (right _) => q end.

O de forma equivalente:

(ifdec (fdec a b) p q).

Se olvida la información de la prueba para construir la expresión pero podrá ser fácilmente utilizada cuando se trate de demostrar propiedades de esta expresión.

Comenzamos por declarar el axioma de decidibilidad de la igualdad sobre los nombres y probaremos la decidibilidad de la igualdad sobre el conjunto de clases.

Coq < Variable eq_name_dec : (n,m:name){n=m}+{~n=m}.

Coq < Theorem eq_sort_dec : (s,s':sort){s=s'}+{~s=s'}.

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 x, el valor que le queremos asignar v y la memoria m. La clase del valor se denota localmente por s.

Coq < Section Update.

Coq < Variable x : name.

Coq < Variable v : semval.

Coq < Variable mem : memory.

Coq < Local s := (sort_val v).

Coq < Definition update : memory
Coq <   := [m:name][s':sort]
Coq <      (ifdec (eq_sort_dec s s')
Coq <             (ifdec (eq_name_dec x m) v (mem m s'))
Coq <             (mem m s')).

Se muestran ahora las propiedades de base de esta función:

Coq < Theorem update_eq : v=(update x s).

Coq < Theorem update_diff_name :
Coq < (m:name)(s':sort)(~x=m)->(mem m s')=(update m s').

Coq < Theorem update_diff_sort :
Coq < (m:name)(s':sort)(~s=s')->(mem m s')=(update m s').

Después de tener probados los lemas, la sección puede cerrarse. Las construcciones realizadas se exportan parametrizadas por x,v y m.

Coq < End Update.

3.5 Semántica operacional

La siguiente declaración implementa la relación que describe la semántica operacional del lenguaje de comandos tal y como está descrita en la figura 6.

Coq < Inductive semcom : memory->com->memory->Prop
Coq <   := semskip    : (m:memory)(semcom m skip m)
Coq <   | semaff      : (m:memory)(n:name)(s:sort)(v:semval)(e:expr)
Coq <                        (exprval m e v)->(semcom m (aff n e) (update n v m))
Coq <   | semseq      : (m,m1,m':memory)(c,d:com)(semcom m c m1)->(semcom m1 d m')
Coq <                         ->(semcom m (seq c d) m')
Coq <   | semcondtr   : (m,m':memory)(e:expr)(c,d:com)(exprval m e (Bool true))
Coq <                         ->(semcom m c m')->(semcom m (cond e c d) m')
Coq <   | semcondfa   : (m,m':memory)(e:expr)(c,d:com)(exprval m e (Bool false))
Coq <                         ->(semcom m d m')->(semcom m (cond e c d) m')
Coq <   | semwhiletr : (m,m':memory)(e:expr)(c:com)(exprval m e (Bool true))
Coq <                         ->(m1:memory)(semcom m c m1)
Coq <                         ->(semcom m1 (while e c) m')
Coq <                         ->(semcom m (while e c) m')
Coq <   | semwhilefa : (m:memory)(e:expr)(c:com)(exprval m e (Bool false))
Coq <                         ->(semcom m (while e c) m).

3.6 Semántica axiomática

Nos interesamos finalmente por la semántica axiomática. 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 : expr->Assertion
Coq < := [E:expr][m:memory](exprval m E (Bool true)).

Coq < Definition Isfalse : expr->Assertion
Coq < := [E:expr][m:memory](exprval m E (Bool false)).

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

Coq < Definition ImplAss : Assertion->Assertion->Prop
Coq < := [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 es verdadero en m si P(m[X¬ v]) se satisface, siendo v el valor de la expresión E en la memoria m.

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

Definición de {P}C{Q}

Se define el predicado (trueform P c Q) que corresponde a {P}C{Q} tal y como se describió en la figura 7.

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

4 Referencias

Los formalismos como el Cálculo de Construcciones Inductivas son muy útilies para formalizar nociones semánticas y lógicas. Una de las primeras pruebas de esta naturaleza ha sido efectuada por Samuel Boutin. Se trataba de un esquema de compilación de un mini-ML a la CAM (Categorical Abstract Machine) tal como se describe en el artículo [3]. Yves Bertot ha estudiado la prueba de un compilador de un lenguaje imperativo hacia un lenguaje ensamblador [1].

Les han seguido otras pruebas de compiladores: Delphine Terrasse realizó la prueba de un compilador de Esterel, Pablo Argon ha extraido el núcleo del compilador del lenguaje Electre expresado como la ejecución de las reglas de la semántica. Equipos de investigación de Dassault et Aérospatiale estudian actualmente la formalización de un compilador para el lenguaje Lustre implantado en la herramienta Scade.

La formalización de la lógica de Hoare ha sido efectuada por Thomas Kleymann-Schreiber [20, 14] en el asistente de prueba LEGO cuyo lenguaje se parece al del CCI aquí presentado.

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 F_w'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].

	`skip`
\|	X`:=` E
\|	C₁;C₂
\|	`if` E `then` C₁ `else` C₂
\|	`while` E `do` C