¬ŅPor qu√© la gente no usa m√©todos formales?

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-
PromelaCSP
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- . - , , .

, . , . - , . , .

, , . , , ¬ę ‚ÄĒ ¬Ľ. , - .

Source: https://habr.com/ru/post/437296/


All Articles