Si aprendió métodos formales para el software, ¿qué tan útil lo ha encontrado?

Si ha recibido capacitación en el uso de métodos formales (FM) para la programación:

• ¿Qué tan útil lo has encontrado?
• ¿En qué consistió su entrenamiento de FM (por ejemplo, un curso, un libro)?
• ¿Qué herramientas de FM utilizas?
• ¿Qué ventajas en velocidad / calidad le ha dado en comparación con no usar FM?
• ¿Qué tipo de software creas con FM?
• Y si no usa FM directamente ahora, ¿valió la pena aprender al menos?

Tengo curiosidad por escuchar tantas experiencias / opiniones sobre FM como se pueden encontrar en esta comunidad; Estoy empezando a leerlo y quiero saber más.

Antecedentes

La programación y el desarrollo / ingeniería de software son algunas de las nuevas habilidades / profesiones humanas en la Tierra, por lo que no es sorprendente que el campo sea inmaduro, eso se muestra en la salida principal de nuestro campo, como un código que generalmente es tardío y propenso a errores. La inmadurez de la industria también se muestra por el amplio margen (al menos 10: 1) en la productividad entre los codificadores promedio y superior. Tales hechos tristes están bien cubiertos en la literatura e introducidos por libros como Code Complete de Steve McConnell .

El uso de métodos formales (FM) ha sido propuesto por figuras importantes en software / CS (por ejemplo, el fallecido E. Dijkstra ) para abordar (una de) las causas raíz de los errores: la falta de rigor matemático en la programación. Dijkstra, por ejemplo, abogó por que los estudiantes desarrollen un programa y su prueba juntos .

FM parece ser mucho más frecuente en los planes de estudio de CS en Europa en comparación con los Estados Unidos. Pero en los últimos años, los nuevos enfoques y herramientas "ligeros" de FM como Alloy han llamado la atención. Aún así, FM está lejos del uso común en la industria, y espero recibir algunos comentarios aquí sobre por qué.

Actualizar

A partir de ahora (10/14/2010), de las 6 respuestas a continuación, nadie ha defendido claramente el uso de FM en el trabajo del "mundo real". Tengo mucha curiosidad si alguien puede y lo hará; o quizás FM realmente ilustra la división entre la academia (¡FM es el futuro!) y la industria (FM es en su mayoría inútil).

Absolutamente inútil para cualquier cosa no trivial.

Tuve un curso llamado, acertadamente, "Métodos formales" que se centró en Alloy. No puedo ver el uso de eso en ninguna parte. Tenía otra clase que se centró en el modelado de concurrencia con LTSA, igualmente inútil.

El problema es que la mayoría de los errores y problemas en el software (al menos en mi experiencia) surgen de la complejidad que ocurre por debajo del nivel de abstracción de esas herramientas.

Tengo experiencia en CSP (Comunicación de procesos secuenciales). No para sonar mi propia bocina, pero escribí mi tesis de maestría sobre CSP programada, particularmente "compilando" especificaciones escritas en métodos formales en C ++ ejecutable. Puedo decir que tengo algo de experiencia con métodos formales. Una vez que completé mi título y obtuve un trabajo en la industria, no he estado usando métodos formales en absoluto. Los métodos formales todavía son demasiado teóricos para ser aplicados en la industria. Los métodos formales han encontrado alguna aplicación práctica en el área de sistemas embebidos. Por ejemplo, la NASA usa métodos formales en sus proyectos. Especularía que los métodos formales están muy lejos de ser ampliamente adoptados en la industria. Simplemente no tiene sentido escribir especificaciones de software en métodos formales y luego "interpretarlas por humanos" en el marco de su elección. El inglés simple y los diagramas funcionan mejor para eso, mientras que las pruebas de unidad e integración han estado haciendo un trabajo bastante bueno de "verificar" la corrección del código. Yo creo queLos métodos formales permanecerán en el mundo académico por algún tiempo .

Los diagramas de estado y las redes de Petri son útiles para modelar y analizar protocolos y sistemas en tiempo real. Primero ayudan a diseñar una solución. Segundo, ayudan a encontrar casos de prueba para software emocionante en situaciones muy específicas.

Leí algunos libros sobre métodos formales y apliqué algunos. Mi reacción inmediata fue: "Caramba, estos libros me dicen cómo ser un buen programador, siempre que sea un matemático perfecto". Otra debilidad es que solo puede probar la equivalencia con otra descripción formal. Escribir una especificación formal para un programa equivale a escribir un programa en un lenguaje de nivel superior, y no hay forma de evitar introducir errores en una especificación razonablemente grande.

Nunca he hecho que los métodos formales funcionen a gran escala. Pueden ser útiles para corregir algo pequeño y complicado, y para convencerme de que son correctos. De esa manera, puedo trabajar con bloques de construcción un poco más grandes y, a veces, hacer un poco más.

Una cosa que aprendí que es más útil en general es el concepto de una invariante, una declaración sobre un programa y su estado que siempre es cierto. Todo lo que puedas razonar es bueno.

Como se mencionó anteriormente, no soy un matemático perfecto, por lo que mis pruebas a veces contienen errores. Sin embargo, en mi experiencia, estos tienden a ser grandes errores tontos que son fáciles de atrapar y corregir.

Tomé un curso de posgrado en análisis de programas formales, donde nos enfocamos en la semántica operativa. Hice mi trabajo final sobre el esfuerzo seL4, revisando los métodos formales que usaron. Mi conclusión principal en términos de practicidad fue que tiene un valor marginal. No solo tienes que escribir el programa, también tienes que escribir la prueba. Guau. Dos fuentes de errores. No sólo uno. Además, había una enorme cantidad de restricciones impuestas en el código real. Es muy difícil describir formalmente una computadora física, incluidas las E / S.

Autodidacta yo mismo TLA + el año pasado, lo he estado usando desde entonces. Es una de las primeras herramientas que alcanzo cada vez que comienzo un proyecto. El error que comete la mayoría de las personas es que asumen que los métodos formales son una cosa de todo o nada: o no está utilizando métodos formales o tiene una verificación completa. Sin embargo, hay algo entre ellos: especificación formal , donde verifica que una especificación abstracta de su proyecto no rompa sus invariantes. A diferencia de la verificación, la especificación es lo suficientemente práctica como para usarla en la industria.

Los lenguajes de especificación son más expresivos que los lenguajes de programación. Por ejemplo, aquí hay una especificación PlusCal (muy) simple para un almacén de datos distribuido:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

Este fragmento especifica cinco nodos que se ejecutan simultáneamente, ejecutando transferencias en un orden arbitrario, donde cada transferencia es una pieza de datos arbitraria a un nodo arbitrario. Además, hemos especificado que cualquier transferencia puede fallar y hacer que el nodo se bloquee. ¡Y podemos simular todos estos comportamientos en el verificador de modelos TLA +! De esa forma podemos probar que, independientemente del orden, las tasas de falla, etc., nuestros requisitos aún se mantienen. Hablando de eso, agreguemos un par de requisitos. Primero, que nunca transferimos datos a un nodo fuera de línea:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

En nuestra versión simplificada, el verificador de modelos encontrará un estado de falla. También podemos especificar "cualquier dato dado está en al menos un nodo en línea":

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

Lo cual también fallará. ¡Buena suerte comprobando esto con una prueba unitaria!

La principal limitación de la especificación es que existe independientemente de su código real. Solo puede decirle que su diseño es correcto, no que lo implementó correctamente. Pero es más rápido especificar que verificar y detecta errores que son demasiado sutiles para probar, por lo que creo que vale la pena el esfuerzo. Casi cualquier código que implique concurrencia o sistemas múltiples es un buen lugar para una especificación formal.

Solía ​​trabajar en un departamento de ICL, antes de que Fujitsu los comprara. Tenían algunos grandes contratos de tipo gubernamental que requerían pruebas de que el software funcionaba como se anunciaba, por lo que construyeron una máquina que tomaría la especificación formal escrita en Z y validaría el código mientras se ejecutaba, con una gran luz verde o roja para aprobar / fallar.

Fue algo sorprendente, pero, como señala el estimado @FishToaster , fue inútil para cualquier cosa no trivial.

1. " ¿Qué tan útil lo has encontrado? "

La aplicación de redes de Petri a la programación de computadoras es muy útil. Creé "Elementos netos y anotaciones", un método basado en redes de Petri (Chionglo, 2014). He estado aplicando el método desde 2014 para escribir programas JavaScript que usan la API Acrobat / JavaScript para aplicaciones de formulario PDF.

2. “ ¿En qué consistió su entrenamiento de FM (por ejemplo, un curso, un libro)? "

Me "entrené" en redes de Petri a través del autoestudio. Leí los capítulos sobre Redes de Petri del libro de texto "Redes de Petri y Grafcet: herramientas para modelar sistemas de eventos discretos" (David y Alla, 1992). También he estado leyendo trabajos de investigación sobre redes de Petri. Después de crear y documentar "Elementos netos y anotaciones", practiqué la aplicación del método durante varias semanas.

3. “ ¿Qué herramientas de FM se utilizan? "

Dibujo diagramas de Petri Net usando PowerPoint. Creo la vista de formulario de anotaciones usando Word. También creo juegos de tokens como aplicaciones de formulario PDF usando Acrobat y Notepad. Después de agregar las entradas al formulario, la traducción de estas entradas al código JavaScript es sistemática. Por lo tanto, debería ser posible automatizar la traducción. Si las "entradas" se agregaron a los objetos gráficos en PowerPoint, entonces también debería ser posible traducirlas sistemáticamente a código JavaScript y también automatizar esta traducción. También utilizo un conjunto de herramientas de trabajo en progreso que realiza estas traducciones y para crear recursos adicionales para crear aplicaciones de formularios PDF (Chionglo, 2018; 2017).

4. “ ¿Qué ventajas en velocidad / calidad te ha dado en comparación con no usar FM? "

Puedo escribir programas JavaScript usando "Elementos y anotaciones netas" más rápido de lo que puedo escribir un programa JavaScript sin usar "Elementos y anotaciones netas". Y para programas grandes, puedo dejar de codificar y volver a codificar más tarde (o mucho más tarde) sin preguntarme dónde continuar (Chionglo, 2019). En algunos casos, puedo escribir programas de JavaScript usando "Elementos y anotaciones de red" pero no puedo escribir los programas de JavaScript sin usar "Elementos y anotaciones de red". Por ejemplo, no podría haber creado implementaciones no recursivas de funciones recursivas sin el uso de "Elementos netos y anotaciones" (Chionglo, 2019b; 2018b; 2016). Esto es cierto con o sin las herramientas de trabajo en progreso.

5. " ¿Qué tipo de software creas con FM? "

Utilizo "Elementos y anotaciones de red" para crear programas de JavaScript que utilizan la API de Acrobat / JavaScript para aplicaciones de formularios PDF. También puedo aplicar el método para crear programas JavaScript para documentos HTML y crear Bocetos Arduino (Chionglo, 2019c; 2019d).

6. " Y si no usa FM directamente ahora, ¿valió la pena aprender al menos? " No aplicable.

Referencias

Chionglo, JF (2019b). Calcular el enésimo término de una relación recursiva: uso de una función no recursiva: una respuesta a una pregunta en Mathematics Stack Exchange. < https://www.academia.edu/38496025/Computing_the_N-th_Term_of_a_Recursive_Relation_Using_a_Non-Recursive_Function_A_Reply_to_a_Question_at_Mathematics_Stack_Exchange >.

Chionglo, JF (2019c). Lógica de control de efecto de llama, simulación y boceto: una respuesta a una solicitud en el foro de la comunidad de Arduino. https://www.academia.edu/40342956/Flame_Effect_Control_Logic_Simulation_and_Sketch_A_Reply_to_a_Request_at_the_Arduino_Community_Forum .

Chionglo, JF (2019). ¿Cómo sigo codificando una aplicación después de un largo descanso? Responda a "¿Cómo sabe dónde se detuvo en sus códigos después de un descanso de 2 semanas?" - Software Engineering Stack Exchange. https://www.academia. : .

Chionglo, JF (2019d). Lógica de control Show-and-Hide: inspirada en una pregunta en Stack Overflow. < https://www.academia.edu/40283015/Show-and-Hide_Control_Logic_Inspired_by_a_Question_at_Stack_Overflow >.

Chionglo, JF (2018b). Un modelo de red de Petri para el factorial de un número: y una función de JavaScript no recursiva para calcularlo. <>.

Chionglo, JF (2018). Crear Hyper Form ™: un flujo de trabajo en progreso: actualización en la investigación de programación neta. https://www.academia.edu/37697498/Create_Hyper_Form_-A_Workflow_in_Progress_Update_on_the_Net_Programming_Research .

Chionglo, JF (2017). Programación en red: una propuesta de investigación: para desarrollar aplicaciones de formularios PDF con PowerPoint y Acrobat. https://www.academia.edu/33374809/Net_Programming_A_Research_Proposal_For_Developing_PDF_Form_Applications_with_PowerPoint_and_Acrobat..

Chionglo, JF (2016). Un modelo de red de Petri para calcular el número de Fibonacci.https://www.academia.edu/31748108/A_Petri_Net_Model_for_Computing_the_Fibonacci_Number.

Chionglo, JF (2014). Elementos netos y anotaciones para la programación de computadoras: cálculos e interacciones en PDF. https://www.academia.edu/26906314/Net_Elements_and_Annotations_for_Computer_Programming_Computations_and_Interactions_in_PDF .

David, R. y H. Alla. (1992) Redes de Petri y Grafcet: herramientas para modelar sistemas de eventos discretos. Upper Saddle, NJ: Prentice Hall.