Todavía se usa. El lenguaje de especificación Z también se usa algunos. Las redes de Petri de colores le permiten modelar el tiempo, lo cual es bueno ya que Z no tiene concepto del tiempo.
Sin embargo, una mirada a proyectos como SEL4 sugiere que la tendencia es hacia el uso de probadores de teóricos, razonadores y generadores de código, típicamente usando lógica de primer orden. Coq, Isabelle, HOL, Why, Ynot, Bedrock, Agda y otros se usan (individualmente o en combinación) para examinar descripciones formales, razonar sobre ellas y generar código (Haskell u OCaml generalmente). También pueden examinar el código escrito en varios lenguajes, como C, Java y SPARK, y crear descripciones formales a partir de ellos.
La idea parece ser que los probadores del teorum solo pueden decirte si lo que crees que estás diciendo es coherente. Los razonadores pueden decirle si su descripción realmente hace lo que cree que hace. Las capas adicionales pueden agregar más empuje a lo que puede verificar y cómo.
- ¿Debería preocuparme que mi amigo se especialice en informática? No creo que alguna vez pueda encontrar el amor. ¿Es algo de lo que debería preocuparme o es su propio problema?
- Se me ocurrió la idea de un proyecto, lo ejecuté y seré el primer autor de la publicación. Mi IP solicitó presentarlo por primera vez en una conferencia antes de su publicación. ¿Debería dejarlo?
- Escuché a personas decir que nunca puedes eliminar cosas permanentemente de Internet, así que mira lo que dices y / o haces. ¿Cómo funciona toda esa teoría?
- Cómo escribir la palabra 'K' cuando el botón 'K' de mi teclado está muerto
- Como estudiante de primer año de CSE interesado en IA y ML, ¿cómo debo proceder?
Dado que el lecho de roca puede analizar el ensamblaje, supongo que debería haber una forma de verificar que el compilador ha generado el código correctamente hasta ahora (que de todos modos es la parte difícil).
SPARK está diseñado específicamente para trabajar con un probador. Omite la sintaxis que aún no es posible probar y le permite incorporar condiciones previas y condiciones posteriores que necesitará el probador además del código. No es el mejor lenguaje, pero es sólido para la codificación formal.
Esto hace que VDM sea algo innecesario, excepto para el trabajo heredado o el trabajo que simplemente no necesita toda esta increíble potencia y puede ser suficientemente descrito por la sintaxis relativamente básica de VDM. No veo el sentido de descargar una docena de herramientas para la extracción, prueba y generación de código, y luego pasar un mes aprendiendo cómo usarlas, si está diseñando un código crítico para un microcontrolador o FPGA que ocupará un lado de un A4 o carta tamaño de papel en VDM. La lógica simplemente no es lo suficientemente compleja como para justificar una fuerte inversión.
