Comprobación estática extendida

La comprobación estática extendida ( ESC ) es un nombre colectivo en informática para una serie de técnicas para comprobar estáticamente la corrección de varias restricciones del programa. ^[1] La ESC puede considerarse una forma extendida de la comprobación de tipos . Al igual que con la comprobación de tipos, la ESC se realiza automáticamente en tiempo de compilación (es decir, sin intervención humana). Esto la distingue de los enfoques más generales para la verificación formal del software, que normalmente 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 la rigurosidad) a costa de introducir algunos falsos negativos (error de subestimación real de ESC, pero que no necesitan la atención del programador o no son el objetivo de ESC). ^{[2] [3]} La ESC puede identificar una serie de errores que actualmente están 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 comprobación estática extendida provienen de varios campos de la informática, incluyendo el análisis de programas estáticos , la simulación simbólica , la comprobación de modelos , la interpretación abstracta , la resolución de SAT y la demostración automatizada de teoremas y la comprobación de tipos . La comprobación estática extendida se realiza generalmente solo a nivel intraprocedimental, en lugar de interprocedimental, para poder escalar a programas grandes. ^[2] Además, la comprobación estática extendida tiene como objetivo informar errores explotando las especificaciones proporcionadas por el usuario , en forma de precondiciones y poscondiciones , invariantes de bucle e invariantes de clase .

Los verificadores estáticos extendidos normalmente operan propagando las postcondiciones más fuertes (respectivamente las precondiciones más débiles ) intraprocedimentalmente a través de un método que comienza desde la precondición (respectivamente la poscondició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 punto para formar una condición de verificación . Un ejemplo de esto es una declaración 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 sea distinto de cero . Todas las condiciones de verificación deben demostrarse como falsas (y, por lo tanto, correctas por medio de un tercero excluido ) para que un método pase la verificación estática extendida (o "no se puedan encontrar más errores"). Normalmente, se utiliza alguna forma de demostrador de teoremas automatizado para descargar las condiciones de verificación.

La comprobación estática extendida fue iniciada en ESC/Modula-3 ^[4] y, posteriormente, en ESC/Java . Sus raíces se originan en técnicas de comprobación estática más simplistas, como la depuración estática ^[5] o lint y FindBugs . Varios otros lenguajes han adoptado ESC, incluidos Spec# y SPARKada y VHDL VSPEC. Sin embargo, actualmente no existe ningún lenguaje de programación de software ampliamente utilizado que proporcione una comprobación estática extendida en su entorno de desarrollo base.

• Lenguaje de modelado Java (JML)

• Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). "Comprobaciones estáticas extendidas para Java". Actas de la conferencia ACM SIGPLAN 2002 sobre diseño e implementación de lenguajes de programación . p. 234. doi :10.1145/512529.512558. ISBN 978-1581134636. Número de identificación del sujeto  47141042.{{cite book}}: CS1 maint: varios nombres: lista de autores ( enlace )
• Babic, Domagoj; Hu, Alan J. (2008). "Calysto". Actas de la 13.ª conferencia internacional sobre ingeniería de software - ICSE '08 . pág. 211. doi :10.1145/1368088.1368118. ISBN 9781605580791.S2CID62868643  .​
• Chess, BV (2002). "Mejora de la seguridad informática mediante la comprobación estática extendida". Actas del Simposio IEEE sobre seguridad y privacidad de 2002. Págs. 160-173. CiteSeerX  10.1.1.15.2090 . Doi : 10.1109/SECPRI.2002.1004369. ISBN . 978-0-7695-1543-4. Número de identificación del sujeto  12067758.
• Rioux, Frédéric; Chalin, Patrice (2006). "Mejora de la calidad de aplicaciones empresariales basadas en la Web con comprobación estática extendida: un estudio de caso". 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. S2CID  14996225.
• Xu, Dana N. (2006). "Comprobaciones estáticas extendidas para Haskell". Actas del taller ACM SIGPLAN de 2006 sobre Haskell . pág. 48. CiteSeerX  10.1.1.377.3777 . doi :10.1145/1159842.1159849. ISBN . 978-1595934895. Número de identificación del sujeto  1340468.
• Leino, K. Rustan M. (2001). "Comprobaciones estáticas extendidas: una perspectiva de diez años". Informática . Apuntes de clase en informática. Vol. 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). "Comprobaciones estáticas extendidas". Informe de investigación de Compaq SRC (159).