En Software Exchange Stack Exchange, vi esta pregunta : "¿Qué está deteniendo la adopción generalizada de métodos formales?" La pregunta se cerró como sesgada, y la mayoría de las respuestas fueron comentarios como "¡Demasiado caro!" o "¡Un sitio no es un avión!" En cierto modo, esto es cierto, pero no explica mucho. Escribí este artículo para dar una imagen histórica más amplia de los métodos formales (FM), por qué no se usan realmente y qué estamos haciendo para corregir la situación.

Antes de comenzar, debe formular algunas condiciones. De hecho, no hay muchos métodos formales: solo unos pocos grupos pequeños . Esto significa que diferentes grupos usan los términos de manera diferente. En términos generales, hay dos grupos de métodos formales: la especificación formal estudia la redacción de especificaciones precisas y sin ambigüedades, y la verificación formal estudia los métodos de prueba. Esto incluye tanto el código como los sistemas abstractos. No solo usamos diferentes términos para el código y los sistemas, a menudo usamos diferentes herramientas para verificarlos. Para hacer las cosas aún más confusas, si alguien dice que está creando una especificación formal, esto generalmente significa verificación del diseño. Y si alguien dice que está haciendo una verificación formal, esto generalmente se refiere a la verificación del código.

Para mayor claridad, dividimos la verificación de verificación de código (CV) y la verificación de diseño (DV) y, de manera similar, dividimos las especificaciones en CS y DS. Dichos términos no se usan comúnmente en la amplia comunidad de FM. Comencemos con CS y CV, luego pasemos a DS y DV.

Además, es posible la verificación parcial , donde solo se verifica un subconjunto de la especificación, o la verificación completa . Esta puede ser la diferencia entre las pruebas de las acusaciones de que "el sistema nunca falla y no acepta la contraseña incorrecta" o "el sistema nunca falla y bloquea la cuenta si ingresa la contraseña incorrecta tres veces". Básicamente, asumiremos que estamos haciendo una verificación completa.

También debe aclarar el tipo de software que estamos formalizando. La mayoría de las personas identifican implícitamente programas altamente confiables como dispositivos médicos y aviones. La gente asume que los métodos formales son ampliamente utilizados para ellos, pero no son necesarios para el resto. Esto es demasiado optimista : el software más confiable no utiliza métodos formales. En cambio, nos centraremos en el software "regular".

Finalmente, el descargo de responsabilidad: no soy un historiador profesional, y aunque intenté verificar cuidadosamente la información, puede haber errores en el artículo. Además, me especializo en especificaciones formales (DS y DV), por lo que hay más posibilidades de error cuando hablo de la verificación del código. Si ves, escríbeme, lo arreglaré (y una cosa más: gano dinero de seminarios sobre TLA + y Alloy, por lo tanto, soy muy parcial hacia estos idiomas; trato de ser lo más objetivo posible, pero entiendes: sesgo es sesgo).

Programación formal

Obteniendo especificación

Antes de probar la exactitud del código, debe obtener el estándar de verdad. Esto significa alguna especificación de lo que debe hacer el código. Debemos saber con certeza que el resultado coincide con la especificación. No es suficiente decir que la lista está "ordenada": no sabemos qué estamos ordenando, qué criterios usamos e incluso qué queremos decir con "ordenar". En cambio, podemos decir: "La lista de enteros l ordenada en orden ascendente para cualquiera de los dos índices i y j, si i < j , entonces l[i] <= l[j] ".

Las especificaciones del código se dividen en tres tipos principales:

1. El primero es escribir declaraciones independientes del código. Escribimos nuestra función de clasificación, y en un archivo separado escribimos el teorema "esto devuelve listas ordenadas". Esta es la forma más antigua de especificación, pero Isabelle y ACL2 aún funcionan de esta manera (ML fue inventado específicamente para ayudar a escribir tales especificaciones).
   
2. El segundo implementa especificaciones en el código en forma de precondiciones y poscondiciones, declaraciones e invariantes. Puede agregar una condición posterior a la función que "el valor de retorno es una lista ordenada". Las especificaciones basadas en reclamos se formalizaron inicialmente como la lógica de Hoar . Aparecieron por primera vez en el lenguaje de programación Euclid a principios de la década de 1970 (no está claro quién comenzó a usarlos: Euclid o SPV , pero hasta donde sé, Euclid se presentó al público antes). Este estilo también se llama programación de contratos , la forma de verificación más popular en la industria moderna (aquí, los contratos se usan como especificaciones de código).
   
3. Finalmente, hay sistemas de tipos. Por correspondencia de Curry - Howard, cualquier teorema matemático o prueba puede codificarse como un tipo dependiente. Definiremos el tipo de listas ordenadas y declararemos el tipo [Int] -> Sorted [Int] para la función.

En Let's Prove Leftpad, puedes ver cómo se ve. HOL4 e Isabelle son buenos ejemplos de las especificaciones del "teorema independiente", SPARK y Dafny son las especificaciones de la "declaración anidada", y Coq y Agda son el "tipo dependiente".

Si observa detenidamente, estas tres formas de especificación de código se comparan con las tres áreas principales de validación automática: pruebas, contratos y tipos. Esto no es una coincidencia. La corrección es un amplio rango, y la verificación formal es uno de sus extremos. A medida que disminuye el rigor (y el esfuerzo) de la verificación, obtenemos verificaciones más simples y más estrechas, ya sea limitando el espacio de estado en estudio, utilizando tipos más débiles o verificando la fuerza en tiempo de ejecución. Entonces, cualquier medio de especificación completa se convierte en un medio de especificación parcial, y viceversa: muchos consideran a Cleanroom una técnica de verificación formal, donde una revisión de código va mucho más allá de las capacidades humanas.

¿Qué especificaciones son correctas?

La verificación verifica que el código se ajusta a la especificación. Surge la pregunta: ¿cómo sabemos que tenemos la especificación correcta? Encontrar la especificación correcta es uno de los mayores problemas en los métodos formales. Esta es también una de las principales objeciones a ellos. Pero los escépticos aquí no quieren decir exactamente lo que los especialistas formales tienen en mente.

Cuando los extraños preguntan: "¿Cómo se obtienen las especificaciones correctas?" Por lo general, piensan en la validación , es decir, especificaciones que no cumplen con los requisitos del cliente. Si demuestra formalmente que su código clasifica la lista, y el cliente realmente quiere Uber para sopas (tm), solo pasó un montón de tiempo. Por ejemplo, solo las iteraciones rápidas y los ciclos de retroalimentación cortos pueden confirmar sus requisitos.

Es cierto que la verificación del código no lo valida. Pero hay dos problemas con este argumento. La primera es que la etapa de aplicar métodos formales simplemente se pospone, pero no desaparece por completo. Después de todas estas iteraciones rápidas, probablemente ya tenga una idea de lo que quiere el cliente. Y luego comienzas la verificación del código. En segundo lugar, aunque no sabemos exactamente qué quiere el cliente, podemos suponer lo que definitivamente no quiere. Por ejemplo, para bloquear accidentalmente el software. No necesitan agujeros de seguridad. Todos están de acuerdo con esto: al final, nadie dice que debe omitir las pruebas unitarias durante las iteraciones. Así que al menos asegúrese de que su sistema de control de versiones no elimine datos de usuario aleatorios (nota: no piense que estoy amargado o algo así).

El problema para encontrar la especificación correcta es más fundamental: a menudo no sabemos qué escribir allí . Pensamos en nuestros requisitos en términos humanos, no matemáticos. Si digo: "El programa debe distinguir los árboles de los pájaros", ¿de qué se trata? Puedo explicárselo a una persona mostrándole un montón de imágenes de árboles y pájaros, pero estos son solo ejemplos concretos, no una descripción de la idea . De hecho, para traducir esto en una especificación formal, es necesario formalizar los conceptos humanos, y este es un problema grave.

No me malinterpretes. Las especificaciones relevantes se pueden definir aquí, y los expertos hacen esto todo el tiempo. Pero escribir las especificaciones apropiadas es una habilidad que necesita ser desarrollada, así como habilidades de programación. Esta es la razón por la cual muchos de los éxitos recientes de la verificación de código se explican por un mapeo claro de lo que queremos en lo que podemos expresar. Por ejemplo, CompCert es un compilador de C. verificado formalmente. La especificación es: "Evitar errores de compilación".

Pero todo esto no tiene nada que ver con la verificación. Cuando tiene una especificación, aún necesita demostrar que el código coincide.

Prueba de especificación

La primera herramienta de verificación de código es el método "piense por qué esto es cierto" al estilo Dijkstra, que es principalmente para ALGOL. Por ejemplo, puedo "probar" la corrección de la clasificación por el método de inserción de la siguiente manera:

1. La opción básica : si agrega un elemento a la lista vacía, será el único elemento, por lo que se ordenará.
   
2. Si tenemos una lista ordenada con k elementos y agregamos un elemento, entonces insertamos el elemento para que quede después de todos los números más pequeños y antes de todos los números más grandes. Esto significa que la lista todavía está ordenada.
   
3. Por inducción, la ordenación por inserción ordenará toda la lista.

Obviamente, en realidad, la prueba se verá más rigurosa, pero esta es una idea general. Dijkstra y otros utilizaron este estilo para demostrar la exactitud de muchos algoritmos, incluidos muchos de los conceptos básicos de concurrencia. Este es también el estilo con el que se asocian las palabras de Knuth : "Cuidado con los errores en este código; Solo probé que era correcto, pero no lo empecé ". Puede arruinar fácilmente una prueba matemática para que nadie se dé cuenta. Según algunas estimaciones , aproximadamente el 20% de la evidencia matemática publicada contiene errores. Peter Guttmann tiene un excelente ensayo sobre la evidencia de la salud de un programa ridículo, donde toneladas de código "probado" caen inmediatamente si los ejecuta.

Al mismo tiempo, estudiamos formas de probar automáticamente teoremas matemáticos. El primer programa para probar los teoremas se publicó en 1967 . A principios de la década de 1970, tales programas comenzaron a usarse para probar el código Pascal, y a mediados de la década aparecieron los idiomas formales especiales. El programador formula algunas propiedades del código y luego crea una prueba verificable de que el código tiene estas propiedades. Los primeros programas para probar teoremas simplemente ayudaron a las personas a verificar las pruebas, mientras que las herramientas más sofisticadas podían probar de forma independiente partes del teorema.

Lo que lleva al siguiente problema.

Es difícil obtener evidencia

La evidencia es difícil, y es un trabajo muy desagradable. Es difícil dejar la programación e ir al circo. ¡Sorprendentemente, las pruebas formales de código son a menudo más estrictas que las pruebas escritas por la mayoría de los matemáticos! La matemática es una actividad muy creativa, donde la respuesta al teorema es válida solo si la muestra. La creatividad va mal con el formalismo y las computadoras.

Tome el mismo ejemplo de clasificación de inserción donde aplicamos la inducción. Cualquier matemático comprenderá de inmediato qué es la inducción, cómo funciona en general y cómo funciona en este caso. Pero en el programa para probar los teoremas todo debe ser estrictamente formalizado. Lo mismo ocurre con la prueba por contradicción, la prueba por contraposición, etc. Además, todos los supuestos deben formalizarse, incluso aquellos en los que la mayoría de los matemáticos no se molestan con la prueba. Por ejemplo, a + (b + c) = (a + b) + c . El programa para verificar teoremas a priori no sabe que esto es cierto. Tienes que demostrarlo (difícil), o declararlo como verdad de acuerdo con la ley asociativa de adición (peligroso), o comprar una biblioteca de teoremas de alguien que ya ha podido demostrarlo (costoso). Los primeros programas de prueba de teoremas compitieron en el número de tácticas de prueba incorporadas y bibliotecas de teoremas relacionadas. Uno de los primeros programas SPADE extendidos presentó la biblioteca aritmética completa como la principal ventaja.

A continuación, debe obtener la prueba en sí. Puede confiar esto al programa o escribirlo usted mismo. Por lo general, la definición automática de evidencia no es decidible. Para casos extremadamente estrechos, como la lógica proposicional o la verificación de tipo HM, es "solo" NP-completo. De hecho, nosotros mismos escribimos la mayor parte de la evidencia, y la computadora verifica su corrección. Esto significa que necesita saber bien:

• matematicas
  
• ciencias de la computación;
  
• el área en la que trabaja: compiladores, hardware, etc.
  
• los matices de su programa y especialización;
  
• Los matices del programa para probar los teoremas que utiliza, que en sí mismo es una especialidad completa.

Peor aún, los palos específicos de la computadora se ponen en las ruedas. ¿Recuerdas que dije que era peligroso asumir una ley de adición asociativa? Algunos idiomas no lo cumplen. Por ejemplo, en C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 es INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) , que es indetectable. Suponiendo una adición asociativa en C ++, su prueba será incorrecta y el código se romperá. Debe evitar esta declaración o demostrar que nunca se producirá un desbordamiento de su fragmento en particular.

Puede decir que la suma indefinida es un error, pero necesita usar un lenguaje con enteros no relacionados. Pero la mayoría de los idiomas tienen características específicas que interfieren con la evidencia. Toma el siguiente código:

 a = true; b = false; f(a); assert a; 

¿Es este siempre el caso? No es un hecho Quizás f cambie a . Tal vez cambie el flujo paralelo. Quizás a b asignado un alias a , por lo que cambiarlo también cambiará a (nota: los alias hacen que sea tan difícil escribir evidencia de que John C. Reynolds tuvo que crear una lógica de separación completamente nueva para tratar este problema). Si algo así es posible en su idioma, entonces debe demostrar claramente que esto no sucede aquí. El código limpio ayudará aquí, en otro caso, puede destruir la prueba, ya que obliga al uso de funciones de recursión y de orden superior. Por cierto, ambos son la base para escribir buenos programas funcionales. ¡Lo que es bueno para la programación es malo para la prueba! (Nota: en esta conferencia, Edmund Clark enumeró algunas propiedades que son difíciles de verificar: "puntos flotantes, cadenas, tipos definidos por el usuario, procedimientos, concurrencia, plantillas universales, almacenamiento, bibliotecas ...").

Los verificadores formales tienen un dilema: cuanto más expresivo es el lenguaje, más difícil es probar algo. Pero cuanto menos expresivo es el lenguaje, más difícil es escribir sobre él. Los primeros lenguajes formales de trabajo eran subconjuntos muy limitados de lenguajes más expresivos: ACL2 era un subconjunto de Lisp, Euclid era un subconjunto de Pascal, etc. Y nada de lo que hemos discutido hasta ahora en realidad prueba programas reales, estos son solo intentos de acercamiento a escribir evidencia.

La evidencia es difícil. Pero se está volviendo más fácil. Los investigadores en este campo agregan nuevas heurísticas, bibliotecas de teoremas, componentes probados previamente, etc. El progreso técnico también ayuda: mientras más rápidas sean las computadoras, más rápida será la búsqueda.

Revolución SMT

Una de las innovaciones a mediados de la década de 2000 fue la inclusión de solucionadores SMT en programas para probar teoremas. En términos generales, un solucionador SMT puede convertir (algunos) teoremas matemáticos en problemas de cumplimiento de restricciones. Esto convierte una tarea creativa en una computacional. Es posible que aún necesite proporcionarle problemas intermedios (lemas) como pasos en el teorema, pero esto es mejor que probarlo todo usted mismo. Los primeros solucionadores SMT aparecieron alrededor de 2004, primero como proyectos académicos. Un par de años después, Microsoft Research lanzó el Z3, un solucionador SMT estándar. La gran ventaja del Z3 fue que se volvió mucho más conveniente de usar que otros SMT, que, francamente, no dijeron casi nada. Microsoft Research lo utilizó internamente para ayudar a probar las propiedades del kernel de Windows, por lo que no se limitaron a una experiencia de usuario mínima.

SMT golpeó a la comunidad FM en voz baja porque de repente hizo trivial muchas pruebas simples y le permitió abordar problemas muy complejos. Por lo tanto, las personas podrían trabajar en lenguajes más expresivos, ya que ahora los problemas de las declaraciones expresivas comenzaron a resolverse. Un progreso increíble es evidente en el proyecto IronFleet : usando los mejores solucionadores SMT y un lenguaje de verificación avanzado, ¡Microsoft pudo escribir 5,000 líneas de código Dafny probado en solo 3.7 años-hombre! Este es un ritmo increíblemente rápido: hasta cuatro líneas completas por día (nota: el registro anterior pertenecía a seL4 , cuyos desarrolladores escribieron dos líneas por día en C.

La evidencia es difícil.

¿Por qué se necesita esto?

Es hora de dar un paso atrás y preguntar: "¿Cuál es el punto?" Estamos tratando de demostrar que algún programa cumple con algunas especificaciones. La corrección es un rango. Hay dos partes para la verificación: cuán objetivamente "correcto" es su programa y cuán cuidadosamente verificó la corrección. Obviamente, cuanto más verificado, mejor, pero la verificación vale la pena el tiempo y el dinero. Si tenemos varias restricciones (rendimiento, tiempo de comercialización, costo, etc.), una validación completa no es necesariamente la mejor opción. Entonces surge la pregunta, ¿cuál es la verificación mínima que necesitamos y cuánto cuesta? En la mayoría de los casos, por ejemplo, 90% o 95% o 99% de corrección es suficiente para usted. ¿Quizás debería dedicar tiempo a mejorar la interfaz, en lugar de verificar el 1% restante?

Entonces la pregunta: "¿Es un cheque del 90/95/99% mucho más barato que el 100%?" La respuesta es si. Es bastante cómodo decir que la base del código, que probamos y escribimos bien, es básicamente correcta, excepto por algunas correcciones en la producción, e incluso escribimos más de cuatro líneas de código por día. De hecho, la gran mayoría de las fallas en los sistemas distribuidos podrían haberse evitado con pruebas un poco más exhaustivas. Y es solo una extensión de las pruebas, sin mencionar las pruebas difusas, basadas en propiedades o pruebas de modelos. Puede obtener un resultado realmente sobresaliente con estos simples trucos sin tener que obtener una prueba completa.

¿Qué pasa si escribir y probar no proporcionan una verificación suficiente? Todavía es mucho más fácil cambiar del 90% al 99% que del 99% al 100%. Como se mencionó anteriormente, Cleanroom es una práctica para desarrolladores que incluye documentación exhaustiva, análisis exhaustivo del flujo y amplias revisiones de código. Sin evidencia, sin verificación formal, ni siquiera pruebas unitarias. Pero una Sala Limpia adecuadamente organizada reduce la densidad de defectos a menos de 1 error por 1000 líneas de código en la producción (nota: cifras del estudio de Stavley en Programación hacia un defecto cero > pero siempre sea escéptico y verifique la fuente ). La programación de salas limpias no ralentiza el ritmo de desarrollo, y ciertamente va más rápido que 4 líneas por día. Y Cleanroom en sí es solo uno de los muchos métodos de desarrollo de software altamente confiables que se encuentran entre el desarrollo habitual y la verificación del código. No necesita una verificación completa para escribir un buen software o incluso casi perfecto. Hay momentos en que se necesita, pero para la mayoría de las industrias es una pérdida de dinero.

Sin embargo, esto no significa que los métodos formales sean generalmente poco económicos. Muchos de los métodos altamente confiables mencionados anteriormente se basan en escribir especificaciones de código que usted no prueba formalmente. En términos de verificación, hay dos formas comunes en que la industria se beneficia. Primero, la verificación del diseño en lugar del código, que discutiremos más adelante. En segundo lugar, una verificación parcial del código, que consideraremos ahora.

Verificación parcial de código

Para las tareas cotidianas, es demasiado costoso hacer una verificación completa. ¿Qué tal parcial? Después de todo, puede beneficiarse de la prueba de algunas propiedades de fragmentos de código individuales. En lugar de demostrar que mi función siempre ordena los números correctamente, al menos puedo demostrar que no se repite para siempre y nunca se sale del rango. Esta también es información muy útil. Entonces, incluso la evidencia más simple para los programas en C es una excelente manera de eliminar una gran parte del comportamiento indefinido .

El problema es la accesibilidad . , . , , . , C Java. . , SPARK Ada, SPARK Ada. .

. — : , tail tail, , [a] -> [a] . Rust Pony . SPARK Frama-C , . , : , . , , Rust Haskell, .

. , , . , : - , , , , .

, , . - , - . , , , , , . , , , , . , . , , .

, « , ». , , . ? - ? ? « » :

• , ? ?
  
• ? ? ? ?
  
• ? , ? «» , ?
  
• , ? ?
  
• ? « » ?
  
• GDPR?
  
• .

. , , , . , , , .

, , . , , (: ). (DL), ( , ; « », ).

, DL VDM 1972 . . DL , (CVL). , DL , CVL — . , DL . , DL:

Idioma
Z	-
Promela		CSP
SDL		-

DL , . , . , DL . Praxis ( Altran), «--» — Z- SPARK — . , .

Alloy Chord, -. AWS 35- , TLA+. , , .

- . , , . , , . . - DL, , , .

, , — .

, , . , : (model checker). , , , . , (: , JMBC, , ).

. -, , . -, escriba evidencia, por lo que la barrera de entrada es mucho más baja. Tercero, si el diseño está roto, al verificar el modelo se obtendrá un contraejemplo explícito. Esto hace que sea mucho más fácil corregir el error, especialmente si se requieren 35 pasos para reproducirlo. Intenta encontrarlo tú mismo.

Hay un par de inconvenientes. En primer lugar, estas herramientas no son tan poderosas. En particular, puede encontrar ilimitado (unbounded) , . , : . … , , . , , .

— (state-space explosion). , , , . , (4*3)! / (4!)^3 = 34 650 (). , 4 300 000. , . , ! , . , , .

: . — « » , . ( ) . AWS .

, (: , « » — ). , , .

, , , . ? DV . — , — : .

, — . DL , (: ; . ; , ( ) : ).

, . , , , .

, , - . , , (, , TDD) . , , .

, : TDD , TDD, Haskell , .

, Agile , . . , , Agile, FM. , . , , .

, , .

Resumen

— . , SMT- . - , , .

, . , . - , . , .

, , . , , « — ». , - .