Se pueden usar métodos formales para especificar, probar y generar código para una aplicación. Esto es menos propenso a errores, por lo tanto, se utiliza principalmente en programas críticos / de seguridad.
¿Por qué no lo usamos con más frecuencia para la programación diaria, o en aplicaciones web, etc.?
Referencias
Respuestas:
Un ingeniero es una persona que puede hacer con un dólar lo que cualquier idiota puede hacer con 10.
Restricciones de recursos, limitaciones de presupuesto, limitaciones de tiempo, todas son importantes.
El desarrollo de software utilizando métodos formales suele ser significativamente más costoso y lleva mucho más tiempo que sin él. Además, para muchos proyectos, la parte más difícil es comprender los requisitos del negocio. Todo lo que usa métodos formales lo compra en ese caso es una prueba de que su código corresponde al 100% a su comprensión incompleta e incorrecta de los requisitos comerciales.
Por esa razón, el uso de métodos formales, pruebas, verificación de programas y técnicas similares generalmente se limita a "cosas que importan", es decir, software de aviónica, sistemas de control para equipos médicos, plantas de energía, etc.
fuente
(-1 + 1) + INT_MAX = INT_MAX,-1 + (1 + INT_MAX)es un comportamiento indefinido.¿Programar o no programar?
Para resolver un problema con un producto de software, después de tener una comprensión de los requisitos, puede SEA escribir un programa utilizando lenguajes de programación O especificar el programa utilizando un lenguaje formal y herramientas de generación de código de uso. Este último solo agrega un nivel de abstracción.
¿Hacer las cosas bien o hacer las cosas bien?
El enfoque formal le brinda una prueba de que su software funciona de acuerdo con las especificaciones. Entonces su producto hace las cosas bien. ¿Pero hace lo correcto?
Los requisitos en los que está trabajando pueden ser incompletos o ambiguos. Incluso podrían tener errores. En el peor de los casos, las necesidades reales ni siquiera se expresan. Pero una imagen vale más que mil palabras, solo imágenes de Google para "Lo que quiere el cliente", por ejemplo de este artículo :
El costo de la formalidad.
En un mundo perfecto, tendría requisitos completamente detallados y perfectos desde el principio. Entonces podría especificar completamente su software. Si opta por formal, su código se generará automáticamente para que sea más productivo. Las ganancias de productividad compensarían el costo de las herramientas formales. Y ahora todos usarían métodos formales. Entonces, ¿por qué no lo es?
¡En la práctica, esto rara vez es la realidad! Es por eso que tantos proyectos en cascada fallaron, y por qué los métodos de desarrollo iterativos (ágil, RAD, etc.) tomaron la delantera: pueden manejar requisitos, diseños e implementaciones incompletos e imperfectos y refinarlos hasta que estén bien.
Y aquí viene el punto. Con métodos formales, cada iteración requiere tener una especificación formal completamente consistente. Esto requiere un pensamiento cuidadoso y trabajo adicional, porque la lógica formal no es indulgente y no le gustan los pensamientos incompletos. Los simples experimentos desechables se vuelven caros bajo esta restricción. Y también cada iteración que llevaría a retroceder (por ejemplo, una idea que no funcionó, o un requisito que no se entendió).
En la práctica
Cuando no está obligado a usar métodos formales por razones legales o contractuales, también puede lograr una calidad muy alta sin sistemas formales, por ejemplo, mediante el uso de programación basada en contratos y otras buenas prácticas (por ejemplo, revisión de código, TDD , etc.). No podrá probar que su software funciona, pero sus usuarios disfrutarán de un software de trabajo antes.
Actualización: esfuerzo medido
En la edición de octubre de 2018 de Communications of the ACM hay un artículo interesante sobre el software verificado formalmente en el mundo real con algunas estimaciones del esfuerzo.
Curiosamente (basado en el desarrollo del sistema operativo para equipos militares), parece que producir software probado formalmente requiere 3,3 veces más esfuerzo que con las técnicas de ingeniería tradicionales. Entonces es realmente costoso.
Por otro lado, requiere 2.3 veces menos esfuerzo obtener software de alta seguridad de esta manera que con el software de ingeniería tradicional si agrega el esfuerzo para certificar dicho software a un alto nivel de seguridad (EAL 7). Entonces, si tiene requisitos de alta confiabilidad o seguridad, definitivamente hay un caso de negocios para ir formal.
fuente
Cada programa en cualquier idioma puede considerarse como una especificación formal (equivalente a alguna máquina de torneado). Cualquier "especificación formal" de nivel superior que se utilizará para demostrar la corrección formal también es, simplemente, otro programa. Pero es (típicamente) un programa malo, incompleto, vago, insuficientemente pensado. Y no es coincidencia, generalmente escrito por personas que no saben programar (generalmente son expertos en dominios).
Y así, demostrando que un programa es compatible (produce las mismas respuestas o como lo caracterice) con sus requisitos formales de nivel superior, invariablemente se reduce a cómo se resuelven las ambigüedades en la especificación formal de nivel superior. No hay una buena forma general de hacerlo.
Esa asignación de requisitos de alto nivel a detalles de nivel inferior es la esencia de lo que se trata la programación real. No debería sorprender que el trabajo central que realiza un programador que lee e interpreta las especificaciones no se puede reemplazar con un saludo manual y diciendo "ahora solo vea si este programa de ejemplo cumple con esta especificación formal de alto nivel".
Incluso en los primeros días de la programación lógica, donde este concepto primero parecía tan prometedor (porque tanto la especificación de alto nivel como los programas subyacentes reales podían escribirse en el mismo lenguaje), este problema central resultó intratable.
fuente