El análisis de estado de tipo , a veces llamado análisis de protocolo , es una forma de análisis de programa empleada en lenguajes de programación . Se aplica más comúnmente a lenguajes orientados a objetos. Los estados de tipo definen secuencias válidas de operaciones que se pueden realizar en una instancia de un tipo determinado. Los estados de tipo, como su nombre indica, asocian información de estado con variables de ese tipo. Esta información de estado se utiliza para determinar en tiempo de compilación qué operaciones son válidas para ser invocadas en una instancia del tipo. Las operaciones realizadas en un objeto que normalmente solo se ejecutarían en tiempo de ejecución se realizan sobre la información de estado de tipo que se modifica para que sea compatible con el nuevo estado del objeto.
Los estados de tipo son capaces de representar refinamientos de tipo de comportamiento como "el método A debe invocarse antes de que se invoque el método B , y el método C no puede invocarse en el medio". Los estados de tipo son adecuados para representar recursos que utilizan semántica de apertura / cierre al imponer secuencias semánticamente válidas como "abrir y cerrar" en lugar de secuencias no válidas como dejar un archivo en estado abierto. Dichos recursos incluyen elementos del sistema de archivos, transacciones, conexiones y protocolos. Por ejemplo, los desarrolladores pueden querer especificar que los archivos o sockets deben abrirse antes de que se lean o escriban, y que ya no se pueden leer ni escribir si se han cerrado. El nombre "typestate" proviene del hecho de que este tipo de análisis a menudo modela cada tipo de objeto como una máquina de estados finitos . En esta máquina de estado, cada estado tiene un conjunto bien definido de métodos / mensajes permitidos, y las invocaciones de métodos pueden provocar transiciones de estado. Las redes de Petri también se han propuesto como un posible modelo de comportamiento para su uso con tipos de refinamiento . [1]
El análisis de estado de tipo fue introducido por Rob Strom en 1983 [2] en el lenguaje de implementación de red (NIL) desarrollado en Watson Lab de IBM . Fue formalizado por Strom y Yemini en un artículo de 1986 [3] que describía cómo usar typestate para rastrear el grado de inicialización de variables, garantizando que las operaciones nunca se aplicarían en datos inicializados incorrectamente, y se generalizarían aún más en el lenguaje de programación Hermes .
En los últimos años, varios estudios han desarrollado formas de aplicar el concepto de estado tipográfico a los lenguajes orientados a objetos. [4] [5]
Acercarse
Strom y Yemini (1986) requirieron que el conjunto de estados de tipo para un tipo dado estuviera parcialmente ordenado, de modo que se pueda obtener un estado de tipo inferior a partir de uno superior descartando cierta información. Por ejemplo, una int
variable en C normalmente tiene los estados de tipo " no inicializado " <" inicializado ", y un FILE*
puntero puede tener los estados de tipo " no asignados " <" asignados, pero no inicializados " <" inicializados, pero el archivo no está abierto " <" archivo abierto " . Además, Strom y Yemini requieren que cada uno de los dos estados tipo tenga un límite inferior máximo, es decir, que el orden parcial sea incluso una semirrejilla de encuentro ; y que cada orden tiene un elemento mínimo, siempre llamado "⊥".
Su análisis se basa en la simplificación de que a cada variable v se le asigna un solo estado de tipo para cada punto del texto del programa; si un punto p es alcanzado por dos rutas de ejecución diferentes yv hereda diferentes estados de tipo a través de cada ruta, entonces el estado de tipo de v en p se toma como el límite inferior más grande de los estados de tipo heredados. Por ejemplo, en el siguiente fragmento de C, la variable n
hereda el estado de tipo " inicializado " y " no inicializado " de then
y la parte (vacía) else
, respectivamente, por lo que tiene el estado de tipo " no inicializado " después de la declaración condicional completa.
int n ; // aquí, n tiene typestate "no inicializado" if (...) { n = 5 ; // aquí, n tiene typestate "inicializado" } else { / * no hacer nada * / // aquí, n tiene typestate "uninitialized" } // aquí, n tiene typestate "uninitialized" = major_lower_bound ("initialized", "uninitialized" )
Cada operación básica [nota 1] debe estar equipada con una transición de estado de tipo , es decir, para cada parámetro, el estado de tipo requerido y asegurado antes y después de la operación, respectivamente. Por ejemplo, una operación fwrite(...,fd)
requiere fd
tener typestate " archivo abierto ". Más precisamente, una operación puede tener varios resultados , cada uno de los cuales necesita su propia transición de estado de tipo. Por ejemplo, el código C FILE *fd=fopen("foo","r")
establece fd
el estado de tipo en " archivo abierto " y " no asignado " si la apertura tiene éxito y falla, respectivamente.
Para cada dos estados de tipo t 1 <· t 2 , se debe proporcionar una operación de coerción de estado de tipo única que, cuando se aplica a un objeto de estado de tipo t 2 , reduce su estado de tipo a t 1 , posiblemente liberando algunos recursos. Por ejemplo, fclose(fd)
coacciona fd
el estado de tipo de " archivo abierto " a " inicializado, pero archivo no abierto ".
La ejecución de un programa se denomina typestate-correct si
- antes de cada operación básica, todos los parámetros tienen exactamente el estado de tipo requerido por la transición de estado de tipo de la operación, y
- al finalizar el programa, todas las variables están en typestate ⊥. [nota 2]
Un texto de programa se denomina coherente con el estado de tipo si se puede transformar, agregando las coerciones de estado de tipo adecuadas, a un programa cuyos puntos se pueden etiquetar estáticamente con estados de tipo de modo que cualquier ruta permitida por el flujo de control sea correcta con el estado de tipo. Strom y Yemini proporcionan un algoritmo de tiempo lineal que comprueba la coherencia de tipo-estado de un texto de programa dado y calcula dónde insertar qué operación de coerción, si corresponde.
Desafíos
Para lograr un análisis de estado de tipo preciso y eficaz, es necesario abordar el problema del aliasing . El alias ocurre cuando un objeto tiene más de una referencia o puntero que apunta a él. Para que el análisis sea correcto, los cambios de estado de un objeto dado deben reflejarse en todas las referencias que apuntan a ese objeto, pero en general es un problema difícil rastrear todas esas referencias. Esto se vuelve especialmente difícil si el análisis debe ser modular, es decir, aplicable a cada parte de un programa grande por separado sin tener en cuenta el resto del programa.
Como otro problema, para algunos programas, el método de tomar el límite inferior más grande en las rutas de ejecución convergentes y agregar las correspondientes operaciones de coerción hacia abajo parece ser inadecuado. Por ejemplo, antes de que el return 1
en el siguiente programa, [nota 3] todos los componentes x
, y
y z
de coord
que se inicializan, pero el enfoque Yemini de Strom y de falla en reconocer esto, ya que cada inicialización de un componente struct en el cuerpo del bucle tiene que ser hacia abajo-coaccionado en la reentrada del bucle para cumplir con el estado de tipo de la primera entrada del bucle, a saber. ⊥. Un problema relacionado es que este ejemplo requeriría sobrecargar las transiciones de estado de tipo; por ejemplo, parse_int_attr("x",&coord->x)
cambia un estado de tipo " sin componente inicializado " por " componente x inicializado ", pero también " componente y inicializado " por " componente xey inicializado ".
int parse_coord ( estructura { int x ; int y ; int z ;} * coord ) { int visto = 0 ; / * recuerda qué atributos se han analizado * / while ( 1 ) if ( parse_int_attr ( "x" , & coord -> x )) visto | = 1 ; else if ( parse_int_attr ( "y" , & coord -> y )) visto | = 2 ; else if ( parse_int_attr ( "z" , & coord -> z )) visto | = 4 ; más romper ; si ( visto ! = 7 ) / * falta algún atributo, falla * / devuelve 0 ; ... / * todos los atributos presentes, hacer algunos cálculos y tener éxito * / return 1 ; }
Inferencia de estado de tipo
Hay varios enfoques que buscan inferir estados de tipo a partir de programas (o incluso otros artefactos como contratos). Muchos de ellos pueden inferir typestates en tiempo de compilación [6] [7] [8] [9] y otros extraen los modelos dinámicamente. [10] [11] [12] [13] [14] [15]
Idiomas compatibles con typestate
Typestate es un concepto experimental que aún no se ha trasladado a los lenguajes de programación convencionales. Sin embargo, muchos proyectos académicos investigan activamente cómo hacerlo más útil como técnica de programación diaria. Dos ejemplos son los lenguajes Plaid y Obsidian, que están siendo desarrollados por el grupo de Jonathan Aldrich en la Universidad Carnegie Mellon . [16] [17] Otros ejemplos incluyen el marco de investigación del lenguaje Clara [18] , versiones anteriores del lenguaje Rust y la >>
palabra clave en ATS . [19]
Ver también
Notas
- ^ estos incluyen construcciones de lenguaje, por ejemplo,
+=
en C, y rutinas de biblioteca estándar, por ejemplofopen()
- ^ Esto tiene como objetivo garantizar que, por ejemplo, se hayan cerrado todos los archivos y que
malloc
se hayafree
d. En la mayoría de los lenguajes de programación, la vida útil de una variable puede finalizar antes de la finalización del programa; En consecuencia, la noción de corrección de tipo-estado debe afinarse en consecuencia. - ^ asumiendo que se
int parse_int_attr(const char *name,int *val)
inicializa*val
siempre que tiene éxito
Referencias
- ↑ Jorge Luis Guevara D´ıaz (2010). "Diseño orientado a Typestate - Un enfoque de red de Petri en color" (PDF) .
- ^ Strom, Robert E. (1983). "Mecanismos para la aplicación de la seguridad en tiempo de compilación". Actas del décimo simposio ACM SIGACT-SIGPLAN sobre principios de lenguajes de programación - POPL '83 . págs. 276-284. doi : 10.1145 / 567067.567093 . ISBN 0897910907.
- ^ Strom, Robert E .; Yemini, Shaula (1986). "Typestate: un concepto de lenguaje de programación para mejorar la confiabilidad del software" (PDF) . Transacciones IEEE sobre ingeniería de software . IEEE. 12 : 157-171. doi : 10.1109 / tse.1986.6312929 .
- ^ DeLine, Robert; Fähndrich, Manuel (2004). "Typestates para objetos" . ECOOP 2004: Actas de la 18ª Conferencia Europea de Programación Orientada a Objetos . Apuntes de conferencias en Ciencias de la Computación. Saltador. 3086 : 465–490. doi : 10.1007 / 978-3-540-24851-4_21 . ISBN 978-3-540-22159-3.
- ^ Bierhoff, Kevin; Aldrich, Jonathan (2007). "Comprobación de estado de tipo modular de objetos con alias". OOPSLA '07: Actas de la 22ª Conferencia ACM SIGPLAN sobre Programación Orientada a Objetos: Sistemas, Lenguajes y Aplicaciones . 42 (10): 301–320. doi : 10.1145 / 1297027.1297050 . ISBN 9781595937865.
- ^ Guido de Caso, Victor Braberman, Diego Garbervetsky y Sebastian Uchitel. 2013. Abstracciones de programas basados en la habilitación para la validación del comportamiento. ACM Trans. Softw. Ing. Methodol. 22, 3, artículo 25 (julio de 2013), 46 páginas.
- ^ R. Alur, P. Cerny, P. Madhusudan y W. Nam. Síntesis de especificaciones de interfaz para clases de Java, 32o Simposio de ACM sobre principios de lenguajes de programación, 2005
- ^ Giannakopoulou, D. y Pasareanu, CS, "Generación de interfaz y verificación de composición en JavaPathfinder", FASE 2009.
- ^ Thomas A. Henzinger, Ranjit Jhala y Rupak Majumdar. Interfaces permisivas. Actas del 13º Simposio Anual sobre Fundamentos de la Ingeniería de Software (FSE), ACM Press, 2005, págs. 31-40.
- ^ Valentin Dallmeier, Christian Lindig, Andrzej Wasylkowski y Andreas Zeller. 2006. Comportamiento de objetos de minería con ADABU. En Actas del taller internacional de 2006 sobre análisis de sistemas dinámicos (WODA '06). ACM, Nueva York, NY, EE. UU., 17-24
- ^ Carlo Ghezzi, Andrea Mocci y Mattia Monga. 2009. Sintetizando modelos de comportamiento intensional por transformación gráfica. En Actas de la 31ª Conferencia Internacional sobre Ingeniería de Software (ICSE '09). IEEE Computer Society, Washington, DC, EE. UU., 430-440
- ^ Mark Gabel y Zhendong Su. 2008. Minería simbólica de especificaciones temporales. In Proceedings of the 30th international conference on Software engineering (ICSE '08). ACM, Nueva York, NY, EE. UU., 51-60.
- ^ Davide Lorenzoli, Leonardo Mariani y Mauro Pezzè. 2008. Generación automática de modelos de comportamiento de software. In Proceedings of the 30th international conference on Software engineering (ICSE '08). ACM, Nueva York, NY, EE. UU., 501-510
- ^ Ivan Beschastnikh, Yuriy Brun, Sigurd Schneider, Michael Sloan y Michael D. Ernst. 2011. Aprovechamiento de la instrumentación existente para inferir automáticamente modelos con restricciones invariantes. In Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC / FSE '11). ACM, Nueva York, NY, EE. UU., 267-277
- ^ Pradel, M .; Gross, TR, "Generación automática de especificaciones de uso de objetos a partir de grandes trazas de métodos", Ingeniería de software automatizada, 2009. ASE '09. 24a Conferencia Internacional IEEE / ACM sobre, vol., No., Págs. 371,382, 16-20 de noviembre de 2009
- ^ Aldrich, Jonathan. "El lenguaje de programación Plaid" . Consultado el 22 de julio de 2012 .
- ^ Coblenz, Michael. "El lenguaje de programación de obsidiana" . Consultado el 16 de febrero de 2018 .
- ^ Bodden, Eric. "Clara" . Consultado el 23 de julio de 2012 .
- ^ Xi, Hongwei. "Introducción a la programación en ATS" . Consultado el 20 de abril de 2018 .