La verificación estática extendida ( ESC ) es un nombre colectivo en ciencias de la computación para una variedad de técnicas para verificar estáticamente la corrección de varias restricciones del programa. [1] ESC se puede considerar como una forma extendida de verificación de tipos . Al igual que con la verificación de tipos, ESC se realiza automáticamente en tiempo de compilación (es decir, sin intervención humana). Esto lo distingue de los enfoques más generales para la verificación formal de software, que generalmente se basan en pruebas generadas por humanos. Además, promueve la practicidad sobre la solidez, ya que tiene como objetivo reducir drásticamente el número de falsos positivos(errores sobreestimados que no son errores reales, es decir, ESC sobre rigor) a costa de introducir algunos falsos negativos (error de subestimación de ESC real, pero que no necesitan la atención del programador, o no son el objetivo de ESC). [2] [3] ESC puede identificar un rango de errores que están actualmente fuera del alcance de un verificador de tipos, incluyendo división por cero , matriz fuera de límites , desbordamiento de enteros y desreferencias nulas .
Las técnicas utilizadas en la verificación estática extendida provienen de varios campos de la informática , incluido el análisis de programas estáticos , la simulación simbólica , la verificación de modelos , la interpretación abstracta , la resolución de SAT y la demostración automatizada de teoremas y la verificación de tipos . La verificación estática extendida generalmente se realiza solo a un nivel dentro de un procedimiento (en lugar de uno entre procedimientos) para escalar a programas grandes. [2] Además, la verificación estática extendida tiene como objetivo informar errores mediante la explotación de especificaciones proporcionadas por el usuario, en forma de condiciones previas y posteriores , invariantes de bucle e invariantes de clase .
Los verificadores estáticos extendidos normalmente operan propagando las postcondiciones más fuertes (resp. Las precondiciones más débiles ) intraprocedimiento a través de un método que comienza desde la precondición (resp. Postcondición). En cada punto durante este proceso se genera una condición intermedia que captura lo que se conoce en ese punto del programa. Esto se combina con las condiciones necesarias de la declaración del programa en ese momento para formar una condición de verificación . Un ejemplo de esto es un enunciado que involucra una división, cuya condición necesaria es que el divisor sea distinto de cero. La condición de verificación que surge de esto establece efectivamente: dada la condición intermedia en este punto, debe seguirse que el divisor es distinto de cero . Se debe demostrar que todas las condiciones de verificación son falsas (por lo tanto, correctas mediante un tercero excluido ) para que un método pase la verificación estática extendida (o "no puede encontrar más errores"). Normalmente, se utiliza alguna forma de demostrador de teoremas automatizado para descargar las condiciones de verificación.
Extended Static Checking fue pionera en ESC / Modula-3 [4] y, más tarde, ESC / Java . Sus raíces se originan en técnicas de comprobación estática más simplistas, como depuración estática [5] o Lint (software) y FindBugs . Varios otros lenguajes han adoptado ESC, incluidos Spec # y SPARKada y VHDL VSPEC. Sin embargo, actualmente no existe un lenguaje de programación de software ampliamente utilizado que proporcione una verificación estática extendida en su entorno de desarrollo base.
Ver también
Referencias
- ^ C. Flanagan, KRM Leino, M. Lillibridge, G. Nelson, JB Saxe y R. Stata. "Comprobación estática ampliada para Java". En Actas de la Conferencia sobre diseño e implementación de lenguajes de programación , páginas 234-245, 2002. doi: http://doi.acm.org/10.1145/512529.512558
- ^ a b "Comprobación estática ampliada" . UWTV . Consultado el 1 de febrero de 2012 .[ enlace muerto permanente ]
- ^ Calysto: Comprobación estática extendida escalable y precisa, Domagoj Babic y Alan J. Hu. En Actas de la Conferencia Internacional sobre Ingeniería de Software (ICSE), 2008. doi : 10.1145 / 1368088.1368118
- ^ Un verificador estático extendido para Modula-3, K. Rustan M. Leino y Greg Nelson. En Proceedings of the Conference on Compiler Construction, páginas 302-305, 1998. doi : 10.1007 / BFb0026418
- ^ Detección de errores en la web de invariantes del programa, C. Flanagan, M. Flatt, S. Krishnamurthi. S. Weirich y M. Felleisen, páginas 23-32, 1996, dpi: http://doi.acm.org/10.1145/249069.231387
Otras lecturas
- Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). Comprobación estática ampliada para Java . Actas de la Conferencia sobre Diseño e Implementación de Lenguajes de Programación (PLDI) . pag. 234. doi : 10.1145 / 512529.512558 . ISBN 978-1581134636.CS1 maint: varios nombres: lista de autores ( enlace )
- Babic, Domagoj; Hu, Alan J. (2008). Calysto: Comprobación estática ampliada, escalable y precisa . Actas de la Conferencia Internacional sobre Ingeniería de Software (ICSE) . pag. 211. doi : 10.1145 / 1368088.1368118 . ISBN 9781605580791.
- Ajedrez, BV (2002). Mejora de la seguridad informática mediante comprobación estática ampliada . Actas del Simposio de IEEE sobre seguridad y privacidad . págs. 160-173. CiteSeerX 10.1.1.15.2090 . doi : 10.1109 / SECPRI.2002.1004369 . ISBN 978-0-7695-1543-4.
- Rioux, Frédéric; Chalin, Patrice (2006). "Mejora de la calidad de las aplicaciones empresariales basadas en web con comprobación estática ampliada: un caso de estudio" . Notas electrónicas en informática teórica . 157 (2): 119-132. doi : 10.1016 / j.entcs.2005.12.050 . ISSN 1571-0661 .
- James, Perry R .; Chalin, Patrice (2009). "Comprobación estática extendida más rápida y completa para el lenguaje de modelado Java". Revista de razonamiento automatizado . 44 (1-2): 145-174. CiteSeerX 10.1.1.165.7920 . doi : 10.1007 / s10817-009-9134-9 . ISSN 0168-7433 .
- Xu, Dana N. (2006). Comprobación estática ampliada para Haskell . Actas del taller de ACM sobre Haskell . pag. 48. CiteSeerX 10.1.1.377.3777 . doi : 10.1145 / 1159842.1159849 . ISBN 978-1595934895.
- Leino, K. Rustan M. (2001). Comprobación estática ampliada: una perspectiva de diez años . Informática . Apuntes de conferencias en informática. 2000 . págs. 157-175. doi : 10.1007 / 3-540-44577-3_11 . ISBN 978-3-540-41635-7.
- Detlefs, David L .; Leino, K. Rustan M .; Nelson, Greg; Saxe, James B. (1998). "Comprobación estática ampliada". Informe de investigación de Compaq SRC (159).