La verificación estática extendida ( ESC ) es un nombre colectivo en informática para una variedad de técnicas para verificar estáticamente la exactitud de varias restricciones de programas. [1] ESC puede considerarse 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 enfoques más generales para la verificación formal de software, que normalmente se basan en pruebas generadas por humanos. Además, promueve la practicidad sobre la solidez, en el sentido de que apunta a 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 del ESC real, pero que no necesitan la atención del programador o no son objetivos de ESC). [2] [3] ESC puede identificar una variedad de errores que actualmente están fuera del alcance de un verificador de tipos, incluida la 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 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 nivel intraprocedimiento, en lugar de interprocedimiento, para poder escalar a programas grandes. [2] Además, la verificación estática extendida tiene como objetivo informar errores explotando las especificaciones proporcionadas por el usuario , en forma de condiciones previas y posteriores , invariantes de bucle e invariantes de clase .
Los verificadores estáticos extendidos generalmente operan propagando las condiciones posteriores más fuertes (respectivamente, las condiciones previas más débiles ) intraprocedimiento a través de un método que comienza desde la condición previa (respectivamente, la condición posterior). En cada punto durante este proceso se genera una condición intermedia que captura lo que se sabe 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 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 se pueden encontrar más errores"). Normalmente, se utiliza algún tipo de demostrador de teoremas automatizado para cumplir las condiciones de verificación.
La verificación estática extendida fue pionera en ESC/Modula-3 [4] y, más tarde, ESC/Java . Sus raíces se originan en técnicas de verificació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#, SPARKada y VHDL VSPEC. Sin embargo, actualmente no existe ningún lenguaje de programación de software ampliamente utilizado que proporcione verificación estática extendida en su entorno de desarrollo base.
{{cite book}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )