programming-languages - tendencies - top 10 programming languages
Idiomas específicamente diseñados para facilitar la verificación estática (7)
Muchos idiomas (quizás todos ellos) están diseñados para facilitar la escritura de programas. Todos ellos tienen diferentes dominios y su objetivo es simplificar el desarrollo de programas en estos dominios (C hace que el desarrollo de programas de bajo nivel sea más fácil, Java facilita el desarrollo de la lógica empresarial compleja, etc.) Quizás otros propósitos se sacrifiquen para escribir y mantener los programas de una manera más fácil, más natural y menos propensa a errores.
¿Existen idiomas diseñados específicamente para facilitar la verificación del código fuente, es decir, el análisis estático? Por supuesto, la capacidad de escribir programas comunes para máquinas modernas también debe persistir.
¿Existen lenguajes específicamente diseñados para facilitar la verificación del código fuente?
Este era un objetivo vago de los idiomas CLU y ML, pero el único diseño de idioma que sé que toma realmente la verificación estática es Spark Ada.
El lenguaje de comandos de Dijkstra (como se describe en Disciplina de la programación ) fue diseñado para soportar la verificación estática, pero se suponía que no estaba implementado explícitamente.
El lenguaje Promela de Gerard Holzmann también fue diseñado para el análisis estático por el verificador de modelos SPIN, pero nuevamente no es ejecutable.
La verificación estática es un mal comienzo para esta tarea. Se basa en el supuesto de que es posible verificar la corrección del programa automáticamente. No es factible en el mundo real, y esperar que el programa verifique un código arbitrariamente complejo sin ninguna sugerencia es simplemente tonto. Por lo general, el software para la verificación estática termina requiriendo pistas en todo el código fuente, y al final genera muchos falsos positivos y falsos negativos. Tiene algún nicho, pero eso es todo. (Ver introducción a " Tipos y lenguajes de programación " por Pierce)
Si bien este tipo de herramientas fueron desarrolladas por ingenieros con propósitos simples, la solución real se ha desarrollado en una academia. Se encontró que los tipos en lenguajes de programación tipificados estáticamente son equivalentes a las declaraciones lógicas dado que todo va bien y el lenguaje no tiene algún tipo de mal comportamiento. Esto se denomina " correspondencia de Curry-Howard ", y la incorporación de la lógica en los tipos es la "lógica de Brouwer-Heyting-Kolmogorov ". Las pruebas más potentes solo son posibles en los idiomas con tipos potentes: tipos dependientes . Si olvidamos toda esta terminología por un tiempo, esto significa que podemos escribir programas que contengan pruebas de su propia corrección, y estas pruebas se verifican mientras se compila el programa, sin ningún archivo ejecutable en caso de falla.
El lado positivo de este enfoque es que nunca obtiene falsos negativos , es decir, se garantiza que el programa compilado funciona correctamente de acuerdo con la especificación. Incluso sin pruebas adicionales sobre la especificación, los programas en lenguajes de tipo dependiente son menos propensos a cometer errores, porque las divisiones por cero, las excepciones no controladas y los desbordamientos nunca terminan en un programa ejecutable.
Siempre es tedioso escribir tales pruebas a mano. Para eso hay " tactics ", es decir, programas que generan pruebas de corrección. Estos son casi equivalentes a los programas de verificación estática, pero, a diferencia de ellos, se requieren para generar pruebas formales.
Existe una gama de idiomas de tipo dependiente para diferentes propósitos: Coq , Agda , Idris , Epigram , Cayenne , etc.
Las tácticas se implementan en Coq y probablemente varios idiomas más. También Coq es el más maduro de todos, con infraestructura que incluye bibliotecas como Bedrock .
En caso de que la extracción del código C de Coq no sea suficiente para sus requisitos, puede utilizar ATS , que está a la par con el rendimiento de C.
Haskell emplea una forma débil de la correspondencia de Curry-Howard: funciona bien, a menos que empiece a escribir programas fallidos o de ciclo continuo. En caso de que sus requisitos no sean tan difíciles de escribir pruebas formales, considere usar Haskell.
No lo he usado yo mismo, así que no puedo hablar con ninguna autoridad, pero entiendo que el lenguaje de programación de Eiffel fue diseñado para usar Código por Contratos, lo que haría el análisis estático mucho más fácil. No sé si eso cuenta o no.
Uno de los objetivos de diseño de Ada era respaldar una cantidad certificada de verificación formal. Fue moderadamente exitoso, pero la verificación no despegó exactamente como esperaban. Por suerte Ada es buena para mucho más que eso. Lamentablemente, eso tampoco ha ayudado mucho ...
Hay un subconjunto de Ada llamado Spark que mantiene esto vivo hoy. Praxis vende una suite de desarrollo construida a su alrededor.
Uno tiene dos problemas para "facilitar la verificación del código fuente". Uno es el idioma en el que usted no hace cosas groseras, como los casos arbitrarios (como C). Otro es especificar lo que desea verificar, para eso necesita un buen lenguaje de aserciones.
Si bien muchos idiomas han propuesto dichos lenguajes de afirmación, creo que la comunidad EDA ha estado impulsando el sobre de manera más efectiva con especificaciones temporales. El "Idioma de especificación de propiedad" es un estándar; Puede obtener más información en P1850 Standard for PSL: Lenguaje de especificación de propiedades (IEEE-1850) . Una idea detrás de PSL es que puede agregarla a los lenguajes EDA existentes; Creo que la comunidad EDA se ha ido incorporando a los idiomas de EDA a medida que pasa el tiempo.
A menudo he deseado que algo como PSL se incruste en los programas informáticos convencionales.
Auditors en el lenguaje E proporcionan un medio integrado para escribir análisis de código dentro del propio lenguaje y requieren que alguna sección del código pase alguna verificación estática. También puede interesarle la parte del trabajo relacionada con el trabajo.