Disponible En

Transcript

Comparaci´ on de T´ ecnicas de Especificaci´ on Sem´ antica de Lenguajes de Programaci´ on J. E. Labra Gayo1 , J. M. Cueva Lovelle1 , M. C. Luengo D´ıez1 , A. Cernuda del R´ıo1 , and L. Joyanes Aguilar2 1 Departamento de Inform´ atica, Universidad de Oviedo C/ Calvo Sotelo S/N, 3307, Oviedo, Spain {labra,cueva,candi,guti}@lsi.uniovi.es 2 Universidad Pontificia de Salamanca (Campus de Madrid) Madrid-Espa˜ na, 28040 [email protected] Abstract We compare the main approaches for the semantic specification of programming languages specifying the same set of three languages in the different formalisms and assessing the ideal requirements of non ambiguity, modularity, reusability, automatic prototype generation, proof facilities, flexibility and experience. Keywords Programming Language Semantics, Modularity, Reusability, Proof, Specification Resumen Se comparan las principales t´ecnicas de especificaci´ on sem´ antica de lenguajes de programaci´ on desarrollando la especificaci´ on de un mismo conjunto de tres lenguajes en los diferentes formalismos y valorando su comportamiento respecto a los requisitos ideales de no ambig¨ uedad, legibilidad, modularidad, reusabilidad, generaci´ on autom´ atica de prototipos, facilidades para la demostraci´ on de propiedades, flexibilidad y experiencia. Palabras clave Sem´ antica de Lenguajes de Programaci´ on, Modularidad, Reusabilidad, Demostraci´ on, Especificaci´ on 1 Introducci´ on Lamentablemente, la especificaci´ on de la mayor´ıa de los lenguajes de programaci´on, desde Fortran [3] hasta Java [9], se realiza en lenguaje natural. Las descripciones en lenguaje natural acarrean gran cantidad de problemas como la falta de rigurosidad y la ambig¨ uedad. Si el lenguaje de programaci´on no est´a bien especificado es imposible demostrar propiedades b´asicas de los programas escritos en ´el. Tampoco es posible garantizar si un procesador de un lenguaje implementa dicho lenguaje ni obtener de forma autom´atica dicho procesador a partir de la especificaci´on. Mientras que para la especificaci´ on sint´actica, la notaci´on BNF se utiliza de forma pr´acticamente universal. En el caso de la especificaci´ on sem´antica existen diversas t´ecnicas formales sin que ninguna de ellas haya alcanzado un alto grado de utilizaci´on. En este art´ıculo se compara el comportamiento de las principales t´ecnicas respecto a unos requisitos que se consideran fundamentales: – No ambig¨ uedad. La t´ecnica debe facilitar la creaci´on de descripciones rigurosas. – Demostraci´ on. La herramienta debe tener una base matem´atica que permita la posterior demostraci´on de propiedades de los programas escritos en el lenguaje especificado. – Prototipo. Deber´ıa ser posible obtener prototipos ejecutables de los lenguajes que se dise˜ nan de forma autom´atica. – Modularidad sem´ antica. La descripci´ on de un lenguaje debe poder realizarse de forma incremental. Al a˜ nadir nuevas caracter´ısticas computacionales a un lenguaje, no debe ser necesario retocar las definiciones que no dependan de dichas caracter´ısticas. Por ejemplo, al a˜ nadir variables a un lenguaje de expresiones aritm´eticas, las especificaciones realizadas para las expresiones aritm´eticas no deber´ıan verse afectadas. – Reusabilidad. La herramienta debe facilitar la reutilizaci´on de descripciones en diferentes lenguajes. Deber´ıa ser posible disponer de una librer´ıa de descripciones sem´anticas de caracter´ısticas que pudiesen a˜ nadirse o eliminarse a un lenguaje de forma sencilla. Un ejemplo ser´ıa la descripci´ on sem´ antica de expresiones aritm´eticas. Existen multitud de lenguajes que admiten este tipo de expresiones y la descripci´on de estos lenguajes deber´ıa permitir incorporar tal componente de forma sencilla. – Legibilidad. Las especificaciones deben ser legibles por personas con una formaci´on heterog´enea. La descripci´ on del comportamiento de un lenguaje afecta a todas las personas que intervienen en el proceso de desarrollo de software y lo ideal es que todas esas personas pudiesen comprender la especificaci´ on. – Flexibilidad. La herramienta descriptiva debe adaptarse a la gran variedad de lenguajes y familias de lenguajes existentes. – Experiencia. La herramienta debe ser capaz de describir lenguajes reales. Algunas de las t´ecnicas existentes son aplicables a lenguajes sencillos pero se resienten al ser aplicadas a algunos de los complejos lenguajes existentes en la actualidad. Debe existir, por tanto, cierta experiencia en la aplicaci´on de la t´ecnica de especificaci´ on a lenguajes de programaci´on reales. El fracaso de las t´ecnicas existentes puede deberse a que no cumplen algunas de las caracter´ısticas anteriores. En este art´ıculo se repasan las principales t´ecnicas y se realiza una valoraci´on de su comportamiento respecto a los criterios mencionados. La comparaci´ on utiliza como ejemplo la descripci´on de un sencillo lenguaje de forma incremental. Se parte de un lenguaje de expresiones aritm´eticas b´asicas, se a˜ naden variables y posteriormente se incluyen ´ordenes imperativas y asignaciones. El objetivo es ofrecer un marco com´ un que permite observar las diferencias entre las diferentes t´ecnicas. Por motivos de espacio, no ser´ a posible justificar las descripciones sem´anticas presentadas ni las valoraciones realizadas. En [15] presentamos este mismo estudio con mayor grado de detalle justificando las valoraciones tomadas. 2 Lenguaje Natural A continuaci´ on se describen en lenguaje natural los tres lenguajes que se tomar´an como ejemplo en el resto del art´ıculo. – El lenguaje L1 consiste u ´nicamente en expresiones aritm´eticas simples. La sintaxis abstracta viene dada por: expr : Const Integer | expr + expr — constante num´erica — suma L1 tiene un u ´nico tipo primitivo que representa los n´ umeros enteros. Las expresiones de L1 denotan valores enteros. – El lenguaje L2 a˜ nade variables al lenguaje anterior con la siguiente sintaxis expr : . . . | Var ident — definiciones anteriores de L1 — identificador Sem´anticamente, la evaluaci´ on de una expresi´on con identificadores depende del valor que el identificador x tenga en el momento de la evaluaci´on. Aunque la modelizaci´on del entorno difiere seg´ un el formalismo sem´ antico utilizado, para unificar las diferentes presentaciones, ς denotar´a un valor de tipo State que representar´a el contexto en el que se eval´ uan los identificadores. Tambi´en se supone que se han definido las siguientes funciones: • upd : State → ident → Value → State, upd ς x v devuelve el estado resultante de asignar a x el valor v en el estado ς. 2 • lkp : State → ident → Value, lkp ς x devuelve el valor de v en ς – L3 incorpora ´ ordenes formadas por secuencias y asignaciones comm : ident := expr | comm ; comm | skip 3 — asignaci´ on — secuencia — comando vac´ıo Sem´ antica Operacional En 1981, G. Plotkin [20] desarrolla la sem´ antica operacional estructurada en la cual se especifican las transiciones elementales de un programa mediante reglas de inferencia definidas por inducci´on sobre su estructura. La especificaci´ on de L1 consta u ´nicamente de expresiones aritm´eticas sencillas cuya evaluaci´on proeval ducir´a un valor entero. La sem´ antica operacional define, una funci´on de evaluaci´on : Expr → N que relaciona una expresi´ on con el valor que denota. Las reglas de inferencia son he1 i hConst ni eval eval he1 + e2 i n he2 i v1 eval eval v2 v1 + v2 Al a˜ nadir variables, la funci´ on de evaluaci´on debe modificarse para poder consultar su valor en un eval contexto ς. El nuevo tipo ser´ a : Expr → State → N. Es decir, el significado de una expresi´on ya no ser´a un valor, sino una funci´ on que depende de un contexto ς ∈ State. La regla de inferencia ser´a eval hV ar v, ςi lkp v ς Sin embargo, la modificaci´ on realizada afecta a las definiciones realizadas hasta el momento. As´ı la definici´on de la evaluaci´ on de expresiones aritm´eticas debe modificarse para que tenga la forma he1 , ςi eval he2 , ςi v1 he1 + e2 , ςi eval eval v2 v1 + v2 En L3 se a˜ naden ´ ordenes imperativas que pueden modificar un estado global. El significado de una orden imperativa toma una porci´ on de programa y un estado y devuelve el resto de programa a ejecutar junto con el nuevo estado. step : (Comm × State) → (Comm × State) Las reglas de inferencia ser´an he, ςi hx := e, ςi step eval hc1 , ςi v hskip, upd ς x vi hskip; c, ςi step hc, ςi hc1 ; c2 , ςi step hc01 , ς 0 i step hc01 ; c2 , ς 0 i La sem´antica operacional anterior se denomina tambi´en sem´antica de paso simple (single-step semantics) ya que se especifica la traza de ejecuci´on de cada comando paso a paso. La sem´antica global de un step comando puede obtenerse mediante el cierre transitivo de . La sem´antica natural [11] aparece como una variaci´on de la sem´antica operacional que define transiciones globales en lugar de transiciones elementales. Tambi´en se denomina big-step semantics o sem´ antica de gran paso. Sin embargo, este formalismo tiene los mismos problemas de modularidad y reusabilidad. Recientemente, P. Mosses, inspirando por la sem´antica mon´adica modular, ha propuesto una sem´antica operacional estructurada modular [18] 3 4 Sem´ antica Denotacional En sem´antica denotacional el comportamiento del programa se describe modelizando los significados mediante entidades matem´ aticas b´ asicas. El estudio denotacional de lenguajes de programaci´on fue propuesto originalmente por C. Strachey en 1967 [21] utilizando λ-c´alculo. Posteriormente D. Scott y C. Strachey colaboran en 1969 para establecer las bases te´oricas utilizando teor´ıa de deminios. La descripci´on del lenguaje L1 se realizar´ a mediante la funci´ on E : Expr → N. E [[Const n]] = n E [[e1 + e2 ]] = E [[e1 ]] + E [[e2 ]] En el caso de L2 , al a˜ nadir variables al lenguaje, es necesario modificar la funci´on de evaluaci´on para que el valor de las variables se obtenga del contexto ς. La funci´on de evaluaci´on ser´a E : Expr → State → N. E [[V ar v]]ς = lkp v ς El cambio anterior obliga a modificar todas las definiciones anteriores para que tengan en cuenta el nuevo argumento: E [[Const n]]ς = n E [[e1 + e2 ]]ς = E [[e1 ]]ς + E [[e2 ]]ς Para capturar la sem´ antica denotacional de las ´ordenes imperativas se utilizar´a una nueva funci´on sem´antica C : Comm → State → State. Es decir, la ejecuci´on de un comando denota una funci´on que, dado un estado inicial, devuelve un estado final. C [[skip]]ς = ς 5 C [[x := e]]ς = upd ς x (E [[e]]ς) C [[c1 ; c2 ]]ς = C [[c2 ]](C [[c1 ]]ς) Sem´ antica Axiom´ atica La sem´antica axiom´ atica [8] consiste en definir una serie de reglas de inferencia que caracterizan las propiedades de las diferentes construcciones del lenguaje. Ha alcanzado gran popularidad en medios acad´emicos, existiendo numerosos libros de texto en los que se describe con mayor detalle [6,1] La utilizaci´on de sem´ antica axiom´ atica para la descripci´on de lenguajes de programaci´on se presenta en [24,10]. Se utilizan aserciones y ternas de Hoare basadas en precondiciones y postcondiciones. Una aserci´ on es una f´ormula P de l´ ogica de predicados que toma un valor booleano en un contexto ς, el cual se denota como [[P]](ς) Una terna de Hoare es una expresi´ on de la forma {P }C{Q} donde P y Q son aserciones y C es una sentencia. P se denomina precondici´ on y Q se denomina postcondici´ on. Normalmente, este formalismo se emplea a posteriori, es decir, una vez definido el lenguaje, se estudia su sem´antica axiom´atica. A continuaci´ on se exponen las reglas de inferencia de las ´ordenes imperativas. {P }skip{P } {P (x/e)}x := e{P } {P }c1 {Q} {Q}c2 {R} {P }c1 ; c2 {R} Con este formalismo se facilita la demostraci´on de propiedades de los programas, adem´as de la verificaci´on a posteriori. 6 Sem´ antica Algebraica La sem´antica algebraica aparece a finales de los a˜ nos 70, a partir de los trabajos desarrollados para la especificaci´on algebraica de tipos de datos. Matem´aticamente, se basa en el ´algebra universal, tambi´en llamada l´ogica ecuacional. Una especificaci´ on algebraica permite definir una estructura matem´atica de forma abstracta junto con las propiedades que debe cumplir. Existen m´ ultiples lenguajes de especificaci´on algebraica como ASL, Larch, ACT ONE, Clear, OBJ [5], etc. Una especificaci´on algebraica consiste en dos partes: 4 – La signatura define los g´eneros (sorts) que se est´an especificando, as´ı como los s´ımbolos de operaciones sobre dichos g´eneros y sus funcionalidades. – Los axiomas son sentencias l´ ogicas que definen el comportamiento de las operaciones. Habitualmente se utilizan una serie de ecuaciones, estableciendo una l´ogica ecuacional. El siguiente m´ odulo define una espec´ıficaci´on algebraica de valores enteros. obj Int is sort Int op 0 : → Int op succ : Int → Int op + : Int Int → Int vars x , y eq x + 0 = x eq x + succ y = succ (x + y) endo La especificaci´ on algebraica del lenguaje formado por espresiones aritm´eticas es similar a la sem´antica denotacional. obj Expr is pr Int subsort Int < Expr op + : Expr Expr → Expr op eval : Expr → Int var n e1 e2 : Expr eq eval n = n eq eval (e1 + e2 ) = eval e1 + eval e2 endo — prInt importa la especificaci´on de enteros — Indica que un entero es una expresi´on La modelizaci´ on de variables requiere una especificaci´on algebraica del contexto de evaluaci´on. La especificaci´on de expresiones con variables ser´a entonces obj VExpr is pr State, pr Expr subsort Var < Expr op eval : State Var → Int var x : Var , var ς : State eq eval ς x = lkp ς x endo Las funciones de evaluaci´ on anteriores ya no sirven, puesto que no ten´ıan en cuenta el estado y deben modificarse. La inclusi´ on de ´ ordenes imperativas en L3 se modeliza de la siguiente forma obj Comm is pr Expr , pr State sort Comm op := : Var Expr → Comm op ; : Comm Comm → Comm op exec : State Comm → State var ς : State, vars c1 c2 : Comm, var x : Var , var e : Expr eq exec ς (x := e) = upd ς x (eval ς e) eq exec ς (c1 ; c2 ) = exec (exec ς c1 ) c2 endo 5 7 M´ aquinas de Estado Abstracto Las m´aquinas de estado abstracto o Abstract State Machines (ASM) definen un algoritmo mediante una abstracci´on del estado sobre el que se trabaja y una serie de reglas de transici´on entre elementos de dicho estado. Originalmente, se denominaban evolving algebras y fueron desarrolladas por Y. Gurevich [7]. Las m´aquinas de estado abstracto pueden considerarse una evoluci´on de la sem´antica operacional que trabajan con un nivel de abstracci´ on cercano al algoritmo que se est´a definiendo. Para la descripci´ on sem´ antica del lenguaje imperativo, se toma como modelo la especificaci´on de Java [2] simplific´ andola para el ejemplo. La especificaci´ on parte de un ´ arbol que representa la sintaxis abstracta del programa. La sem´antica se considera como un recorrido sobre dicho ´arbol. En cada nodo, se ejecuta la tarea especificada y luego, el flujo de control prosigue con la siguiente tarea. Se utilizan una serie de funciones din´amicas para representar el estado de la computaci´ on. Una funci´on din´amica es una funci´on que puede modificarse durante la ejecuci´ on. Para la especificaci´ on del lenguaje de expresiones aritm´eticas se utiliza una funci´on din´amica val : Expr → Int que almacena el valor intermedio a devolver. Las reglas de transici´on ser´an las siguientes if task is num then val (task ) := num proceed if task is e1 + e2 then val (task ) := val (e1 ) + val (e2 ) proceed Para la inclusi´ on de variables, se a˜ nade la funci´on din´amica loc : Var → Value que devuelve el valor actual de una variable. La regla de transici´on ser´a: if task is var then val (task ) := loc(var ) proceed La regla de transici´ on para ´ ordenes imperativas ser´a if task is skip then proceed if task is x := e then loc(x ) := val (e) proceed En el caso de la estructura secuencial c1 ; c2 la regla de transici´on simplemente continua con c1 tras haber modificado la funci´ on de ejecuci´ on para que, al finalizar c1 contin´ ue la ejecuci´on con c2 . 8 Sem´ antica de Acci´ on La sem´ antica de acci´ on fue propuesta por Mosses [19] con el fin de crear especificaciones sem´anticas m´as legibles, modulares y utilizables. La sem´antica de un lenguaje se especifica mediante acciones, que expresan computaciones. Sint´ acticamente, la notaci´on de acciones tiene bastante libertad simulando un lenguaje natural restringido. Internamente, dicha notaci´on se transforma en sem´antica operacional estructurada. Existen acciones primitivas y combinadores de acciones. Un combinador de acciones toma una o m´as acciones y genera una acci´ on m´ as compleja. La modelizaci´on de los diferentes tipos de acciones se realiza mediante facetas. Existen varios tipos de facetas como la faceta b´asica, funcional, declarativa, imperativa y comunicativa, y cada faceta captura una determinada noci´on computacional. A continuaci´ on se incluyen las sem´ anticas utilizadas para el lenguaje aritm´etico • evaluate :: Expr → action [giving Integer] 6 (1) (2) evaluate [[ n:Numeral ]] = give n evaluate [[ E1 :Expr “+” E2 :Expr ]] = evaluate E1 and evaluate E2 then give sum(given Integer#1,given Integer#2) Al especificar L2 se a˜ naden identificadores cuyo valor depende del contexto. (1) evaluate [[ x : Ident ]] = give value stored in cell bound to x El lenguaje L3 podr´ıa especificarse de la siguiente forma • execute :: Comm → Action [completing storing] execute [[ “skip” ]] = complete (2) execute [[ x:Ident “:=” E:Expr ]] = give the cell bound to x and evaluate E then store the given Value#2 in the given cell#1 (3) execute [[ C1 :Comm “;” C2 :Comm ]] = execute C1 and then execute C2 (1) Aunque pueda parecer que las descripciones en sem´antica de acci´on son realizadas en lenguaje natural. En realidad, se utiliza un lenguaje formal con una sintaxis bastante flexible que permite utilizar identificadores formados por varias palabras pero que son reconocidos por el analizador sint´actico sin que se produzcan ambig¨ uedades. 9 Sem´ antica Mon´ adica Modular La sem´antica mon´ adica modular [17,16] surge a partir de la utilizaci´on de m´onadas y transformadores de m´onadas para describir una sem´ antica denotacional modular. Intuitivamente, una m´onada separa una computaci´on del valor devuelto por dicha computaci´on. Con dicha separaci´ on se favorece la modularidad sem´antica, pudiendo especificarse caracter´ısticas computacionales de los lenguajes de forma separada. Aunque el concepto de m´onada deriva de Teor´ıa de Categor´ıas, en sem´antica de lenguajes, una m´ onada M puede considerarse como un tipo abstracto con dos operaciones return : α → M α (=) : M α → (α → M β) → M β Existen diversos tipos de m´ onadas que a˜ naden nuevas operaciones. Por ejemplo, la m´onada que admite acceso a un entorno Env incorpora las operaciones rdEnv : M Env inEnv : Env → M α → M α y la m´onada que admite la modificaci´on de un estado State incluye las operaciones fetch : M State set : State → M State La interacci´ on entre las diferentes operaciones se especifica mediante axiomas observacionales que delimitan su significado y permiten demostrar propiedades. Un problema de esta t´ecnica es que, en 7 general, no es posible componer dos m´ onadas para obtener una nueva m´onada. Una soluci´on ser´a la utilizaci´on de transformadores de m´ onadas que toman una m´onada My la convierten en una nueva m´onada M’ a˜ nadiendo nuevas operaciones. En la especificaci´ on del lenguaje L1 la funci´on de evaluaci´on tendr´a el tipo E : Expr → M Int, es decir, toma una expresi´ on y devuelve una computaci´on M que al ejecutarse devuelve un entero. Las definiciones sem´ anticas ser´ an: E [[Const n]] = return n E [[e1 + e2 ]] = E [[e1 ]]=λv1 → E [[e2 ]]=λv2 → return v1 + v2 En L2 se incluyen variables cuyo valor debe obtenerse de un entorno. Ser´a necesario modificar la estructura computacional mediante un transformador de m´onadas. E [[V ar x]] = rdEnv =λς → return(lkp ς x ) En el lenguaje L3 aparecen las ´ ordenes imperativas. Para su modelizaci´on sem´antica se debe modificar de nuevo la estructura computacional, incorporando un transformador de m´onadas que a˜ nada un estado actualizable. El tipo ser´ a C : Comm → M (), es decir, realiza computaciones, pero no devuelve ning´ un valor. Las definiciones sem´ anticas ser´ıan: C [[skip]] = return () C [[c1 ; c2 ]] = C [[c1 ]]=λ → C [[c2 ]] C [[x := e]] = E [[e]]=λv → fetch=λς → set (upd ς x v ) 10 Sem´ antica Mon´ adica Reutilizable La sem´antica mon´ adica reutilizable a˜ nade conceptos de programaci´on gen´erica a la sem´ antica mon´adica modular facilitando la reusabilidad de las descripciones de este formalismo. Ha sido utilizada para la descripci´on de lenguajes imperativos [14], funcionales [12], orientados a objetos [15] y de programaci´on l´ogica [13]. La descripci´ on utiliza functores no recursivos que capturan la estructura sint´actica y ´algebras que toman como conjunto soporte la estructura computacional. Posteriormente, el int´erprete se obtiene de forma autom´ atica como un catamorfismos sobre la suma de las ´algebras definidas. Las definiciones sem´ anticas ser´ an ϕE : E(M N) → M N ϕE (Num n) = return n ϕE (e1 + e2 ) = e1 =λv1 → e2 =λv2 → return v1 + v2 El valor de una variable debe buscarse en el entorno. La modelizaci´on de este concepto sem´antico se realiza transformando la m´ onada anterior en una m´onada lectora del entorno. ϕV : V(M N) → M N ϕV (Var x ) = rdEnv =λς → return(lkp ρ x ) La incorporaci´ on de comandos supone utilizar dos categor´ıas sint´acticas, una de expresiones y otra de o´rdenes aritm´eticas. Las expresiones pueden reutilizarse convirtiendo el functor en un bifunctor. 8 A nivel sem´antico, la posibilidad de utilizar un estado modificable durante la ejecuci´on requiere u ´nicamente transformar la m´ onada que define la estructura computacional. ψC ψC (Skip) ψC (c1 ; c2 ) ψC (x := e) 11 : C (M N) (M ()) → (M ()) = return () = c1 =λ → c2 = e=λv → fetch=λς → set (upd ς x v ) Conclusiones En la tabla 1 se presenta una valoraci´ on comparada de las diferentes t´ecnicas de especificaci´on sem´antica. La comparaci´ on entre estas caracter´ısticas es cualitativa, no cuantitativa, intentando huir de valoraciones num´ericas que podr´ıan dar lugar a juicios equ´ıvocos. Se utiliza el siguiente esquema: si el formalismo X admite la caracter´ıstica Y , entonces en la celda (X , Y ) aparece el s´ımbolo ↑. Si admite la caracter´ıstica de forma parcial, se utiliza el s´ımbolo ≈. Finalmente, si no admite la caracter´ıstica, no se pone nada. NAM MOD REU DEM PRO LEG FLE EXP Leng. Natural ↑ ↑ ≈ ↑ ↑ Sem. Operacional Est. ↑ ≈ ≈ ≈ ↑ ↑ Sem. Natural ↑ ≈ ↑ ≈ ↑ ↑ Sem. Denotacional ↑ ↑ ≈ ↑ ≈ Sem. Axiom´ atica ≈ ↑ ≈ ↑ Sem. Algebraica ↑ ≈ ↑ ↑ ≈ ≈ ≈ M´ aq. Estado Abstracto ↑ ↑ ≈ ≈ ↑ ≈ ↑ Sem. de Acci´ on ↑ ↑ ≈ ≈ ↑ ↑ ≈ ≈ Sem. Mon´ adica Modular ↑ ↑ ↑ ≈ ↑ Sem. Mon´ adica Reutilizable ↑ ↑ ↑ ↑ ↑ ↑ Tabla 1. Tabla comparativa entre t´ecnicas de especificaci´ on sem´ antica – No Ambig¨ uedad (NAM). Evidentemente, el lenguaje natural es ambig¨ uo y poco riguroso. En ese sentido, todos los formalismos estudiados resuelven el problema de la ambig¨ uedad mediante especificaciones de ra´ız matem´ atica. En el caso de la sem´antica axiom´atica pueden surgir problemas de ambig¨ uedad debido a la no especificaci´on de ciertas caracter´ısticas. – Modularidad sem´ antica (MOD). La modularidad sem´antica es alcanzada en el lenguaje natural debido a la falta de rigurosidad, que permite realizar descripciones ligeramente vagas, que se adaptan a la introducci´ on de nuevas caracter´ısticas sem´anticas independientes. Los formalismos tradicionales no resuelven este problema y quiz´ as sea ´esa una de las razones de su escasa utilizaci´on pr´actica [23]. Las m´aquinas de estado abstracto resuelven el problema mediante la especializaci´on de la abstracci´on del estado, la sem´ antica de acci´ on lo resuelve mediante la especializaci´on de facetas y las sem´anticas mon´adica modular y reutilizable lo resuelven mediante transformadores de m´onadas. – Componentes sem´ anticos reutilizables (REU). El lenguaje natural, por la misma raz´on anterior, admite la reutilizaci´ on de las especificaciones, las cuales siguen la modelizaci´on conceptual de las caracter´ısticas del lenguaje. Los formalismos tradicionales no atacan este problema y por tanto, tampoco lo resuelven. La sem´ antica algebraica contiene potentes mecanismos de reutilizaci´on, aunque las especificaciones realizadas en este formalismo son monol´ıticas [5]. En la sem´antica de acci´on se han planteado soluciones al problema, aunque no han sido implementadas [4] y parece que su implementaci´on traer´ıa 9 – – – – – problemas de inconsistencias. La sem´ antica mon´adica reutilizable resuelve el problema admitiendo la definici´on y reutilizaci´ on de componentes sem´anticos que pueden incorporarse a un lenguaje de forma independiente. El sistema no produce inconsistencias al separar en categor´ıas sint´acticas diferentes las entidades que se van incorporando. Demostraci´ on de propiedades (DEM). El lenguaje natural no admite la demostraci´on de propiedades de los lenguajes especificados. Las otras t´ecnicas admiten la demostraci´on de propiedades con mayor medida cuanto menos operacionales sean. La sem´antica axiom´ atica y algebraica facilitan el razonamiento formal al utilizar axiomas independientes de una implementaci´on particular. De la misma forma, la sem´antica denotacional describe el lenguaje mediante conceptos matem´ aticos abstractos con los que se pueden realizar demostraciones. La demostraci´ on de propiedades en sem´antica de acci´on es dif´ıcil ya que la notaci´on de acciones se basa en sem´ antica operacional. En [22] se plantea la relaci´on entre la sem´antica de acci´on y la sem´antica mon´ adica modular. Para ello define la notaci´on de acciones mediante transformadores de m´onadas en lugar de utilizar sem´ antica operacional estructurada. Las sem´anticas mon´ adica modular y reutilizable tienen su base en la combinaci´on entre sem´antica denotacional y sem´ antica algebraica, ya que los conceptos del lenguaje se definen a partir de m´onadas, los cuales tienen un comportamiento observacional definido a partir de axiomas. Prototipos (PRO). Los sistemas operacionales facilitan la creaci´on de prototipos. De hecho, todos los sistemas que tienen una base operacional (sem´antica operacional estructurada, sem´antica natural, m´aquinas de estado abstracto y sem´antica de acci´on) permiten el desarrollo de prototipos. La sem´antica axiom´ atica tradicional no permite esta posibilidad, ya que la definici´on de los axiomas se realiza precisamente teniendo en cuenta la independencia de la implementaci´on. A diferencia de ella, la sem´ antica algebraica, al basarse el l´ogica ecuacional, permite desarrollar prototipos mediante t´ecnicas de reescritura. Por la misma raz´on, las sem´anticas mon´adica modular y reutilizable permiten obtener prototipos de forma directa. Legibilidad (LEG). El u ´nico sistema que ha prestado gran importancia a la legibilidad evitando adem´as los problemas de ambig¨ uedad del lenguaje natural, es la sem´antica de acci´on. Podr´ıa ser interesante incorporar las facilidades sint´acticas de la sem´ antica de acci´on en la sem´antica mon´adica reutilizable mediante la definici´ on de un metalenguaje de dominio espec´ıfico. Flexibilidad (FLE). Las t´ecnicas operacionales y denotacionales se adaptan a la definici´on de lenguajes de diferentes paradigmas. Sin embargo, es m´as dif´ıcil desarrollar una sem´antica axiom´atica para nuevos lenguajes y paradigmas, lo cual requiere cierta experiencia. Como ya se ha indicado, la sem´ antica mon´adica reutilizable ha sido utilizada para la descripci´on de lenguajes en los paradigmas imperativo, l´ogico, funcional y orientado a objetos. Experiencia (EXP). Las t´ecnicas tradicionales, especialmente, las t´ecnicas de base operacional, han sido aplicadas a la descripci´ on de lenguajes reales. En teor´ıa, la sem´antica mon´adica reutilizable podr´ıa utilizarse para la especificaci´ on de lenguajes de programaci´on pr´acticos. Referencias 1. R. Backhouse. Program Construction and Verification. Prentice Hall International, Englewood Cliffs, NJ, 1986. 2. E. B¨ orger and W. Schulte. Programmer friendly modular definition of the semantics of java. In J. Alver-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998. 3. Computer and Business Equipment Manufacturers Association, editors. Programming Language FORTRAN. American National Standard Institute, Inc., 1978. X3.9-1978, Revision of ANSI X3.9-1966. 4. K. Doh and P. Mosses. Composing programming languages by combining action-semantics modules. In M. van den Brand, M. Mernik, and D. Parigot, editors, First workshop on Language, Descriptions, Tools and Applications, Genova, Italy, April 2001. 5. Joseph A. Goguen and Grant Malcolm. Algebraic Semantics of Imperative Programs. Foundations in Computer Science. The MIT Press, 1996. 6. D. Gries. The Science of Programming. Springer-Verlag, New York, 1981. 10 7. Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. B¨ orger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995. 8. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, October 1969. 9. Bill Joy, Guy Steele, Jame Gosling, and Gilad Bracha. The Java Language Specification. Addison-Wesley, 2 edition, 2000. 10. B. L. Kurtz K. Slonneger. Formal Syntax and Semantics of Programming Languages. Addison-Wesley, 1995. 11. G. Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, volume 247, pages 22–39. Springer-Verlag, 1987. 12. J. E. Labra, J. M. Cueva, M. C. Luengo, and A. Cernuda. LPS: A language prototyping system using modular monadic semantics. In M. van den Brand and D. Parigot, editors, First Workshop on Language Descriptions, Tools and Applications, volume 44, Genova, Italy, April 2001. Electronic Notes in Theoretical Computer Science – Elsevier. 13. J. E. Labra, J. M. Cueva, M. C. Luengo, and A. Cernuda. Specification of logic programming languages from reusable semantic building blocks. In International Workshop on Functional and (Constraint) Logic Programming, Kiel, Germany, September 2001. University of Kiel. 14. J. E. Labra, J. M. Cueva Lovelle, M. C. Luengo D´ıez, and B. M. Gonz´ alez. A language prototyping tool based on semantic building blocks. In Eight International Conference on Computer Aided Systems Theory and Technology (EUROCAST’01), Lecture Notes in Computer Science, Las Palmas de Gran Canaria – Spain, February 2001. Springer Verlag. 15. Jose E. Labra. Modular Development of Language Processors from Reusable Semantic Specifications. PhD thesis, Dept. of Computer Science, University of Oviedo, 2001. In spanish. 16. Sheng Liang and Paul Hudak. Modular denotational semantics for compiler construction. In Programming Languages and Systems – ESOP’96, Proc. 6th European Symposium on Programming, Link¨ oping, volume 1058 of Lecture Notes in Computer Science, pages 219–234. Springer-Verlag, 1996. 17. Sheng Liang, Paul Hudak, and Mark P. Jones. Monad transformers and modular interpreters. In 22nd ACM Symposium on Principles of Programming Languages, San Francisco, CA. ACM, January 1995. 18. P. Mosses. Foundations of modular SOS. Technical Report RS-99-54, BRICS, Dept. of Computer Science, University of Aarhus, 1999. 19. Peter D. Mosses. Action Semantics. Cambridge University Press, 1992. 20. Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981. 21. C. Strachey. Fundamental Concepts in Programming Languages. Higher Order and Symbolic COmputation, 13, April 2000. Reprinted from Lecture notes, International Summer School in Computer Programming at Copenhagen, 1967. 22. Keith Wansbrough. A modular monadic action semantics. Master’s thesis, Department of Computer Science, University of Auckland, February 1997. 23. David A. Watt. Why don’t programming language designers use formal methods? In Seminario Integrado de Software e Hardware - SEMISH’96, pages 1–6, Recife, Brazil, 1996. University of Pernambuco. 24. Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundation of Computing Series. MIT Press, Cambridge, MA, 1993. 11