| CHISPA - CHISPEAR | |
|---|---|
| clase de idioma | paradigma múltiple |
| Apareció en | 1988 |
| Desarrollador | Altran , AdaCore |
| Liberar | 22 (2021 ) |
| sistema de tipos | estático , estricto , seguro , nominativo |
| Implementaciones principales | SPARK Pro, edición SPARK GPL |
| sido influenciado | Diablos , Eiffel |
| Licencia | GPLv3 |
| Sitio web | adaic.org/advantages/spa… |
| sistema operativo | Linux , Microsoft Windows , mac OS |
SPARK ( SPADE Ada Kernel [1] ) es un lenguaje de programación formalmente definido , que es un subconjunto de Ada [2] , diseñado para desarrollar software verificado con un alto nivel de integridad de seguridad . SPARK le permite crear aplicaciones que tienen un comportamiento predecible y brindan alta confiabilidad.
Las versiones de idioma SPARK están relacionadas con las versiones de Ada y se dividen en dos generaciones: SPARK 83, SPARK 95 y SPARK 2005 (Ada 83, Ada 95 y Ada 2005 respectivamente) pertenecen a la primera generación, y SPARK 2014 (Ada 2012) a la segunda. . Esto se debe a que inicialmente los comentarios se utilizaban para indicar especificaciones y contratos , pero a partir de Ada 2012 se empezó a utilizar para ello el mecanismo de aspecto que aparecía en el lenguaje. Esto condujo a un rediseño completo de todo el conjunto de herramientas de lenguaje y al surgimiento de un nuevo verificador GNATprove.
SPARK se utiliza en aviación (motores a reacción Rolls-Royce Trent [3] , aviones Eurofighter Typhoon [4] y Be-200 [5] , sistema UK NATS iFACTS [6] ) y para el desarrollo de sistemas espaciales ( vehículo de lanzamiento Vega , muchos satélites [7] ). También se utiliza para desarrollar sistemas de encriptación [8] y ciberseguridad [9] [10] [11] .
El objetivo del desarrollo de SPARK era preservar las fortalezas de Ada (como el sistema de paquetes y los tipos restringidos) y eliminar todas las construcciones potencialmente inseguras o ambiguas [1] , ya que Ada, a pesar de los objetivos de desarrollo establecidos, resultó ser un lenguaje bastante complejo y que no poseía definiciones formales completas [1] , y algunas de sus partes han causado serias críticas [12] . Los programas SPARK deben ser inequívocos, su comportamiento no debe depender de la elección del compilador [K 1] , las opciones de compilación y el estado del entorno. Para ello, se han introducido algunas restricciones en el lenguaje, entre ellas: el uso de tareas solo es posible en el perfil de Ravenscar; las expresiones no permiten efectos secundarios ; está prohibido utilizar tipos controlados, para los cuales es posible redefinir procedimientos de inicialización y operador de asignación; se prohíbe la combinación de nombres; uso limitado de algunos operadores como goto ; la asignación de memoria dinámica está prohibida (pero se permiten tipos con límites dinámicos y tipos con discriminantes) [2] .
Sin embargo, cualquier programa SPARK aún puede ser compilado por el compilador Ada, lo que le permite mezclar estos lenguajes en un proyecto.
Los desarrolladores de SPARK lograron obtener un lenguaje conveniente para la verificación automática, que tiene una semántica simple, una definición formal estricta, corrección lógica y buena expresividad [1] .
Para un procedimiento que incrementa el valor de alguna variable global por su argumento si es positivo, y por otro en caso contrario, puede escribir la siguiente especificación:
procedimiento Add_to_Total ( Valor : in Integer ) with Global => ( In_Out => Total ), Depende => ( Total => ( Total , Value )), Pre => ( Total < Integer ' Last - ( if Value > 0 then Value else 1 )), Post => ( Total = Total ' Old + ( if Value > 0 then Value else 1 ));El aspecto Global muestra a qué variables globales tiene acceso el procedimiento. En este caso, solo utiliza la variable Total para lectura y escritura. Depende muestra la relación entre variables: el nuevo valor de Total depende de su valor anterior y del valor de Value . Pre - una condición previa, muestra en qué estado debe estar el programa antes de la ejecución del procedimiento; en este caso, la condición previa comprueba si se produce un desbordamiento. Post es una postcondición, muestra el estado del programa después de la ejecución del procedimiento.
Además de los aspectos de las rutinas, existen otras formas de especificar restricciones en el estado de un programa, como declaraciones de verificación:
pragma Afirmar ( Condición );o bucle invariantes:
pragma Loop_Invariant ( Condición );Al mismo tiempo, existen diferencias significativas en la sintaxis para describir contratos para las versiones SPARK de la primera y segunda generación.
La primera generación del lenguaje usó comentarios especiales:
-- Duplicar un número natural. procedimiento Doble ( X : dentro fuera Natural ); --# pre X < Natural'Último / 2; --# publicación X = 2 * X~;Código equivalente para segunda generación:
-- Duplicar un número natural. procedimiento Double ( X : in out Natural ) con Pre => X < Natural ' Last / 2 , Post => X = 2 * X ' Old ;Al verificar programas, se utilizan los siguientes métodos:
Para probar la corrección del programa, para todas las construcciones utilizadas por el programador, como las condiciones previas y posteriores, se crean conjuntos de declaraciones de verificación. El verificador GNATprove también puede, en algunos casos, generar aserciones de verificación por sí mismo. Por lo tanto, se realizarán comprobaciones fuera de los límites de matrices o tipos, desbordamiento y división por cero.
Además, un conjunto de declaraciones de verificación y datos sobre el estado inicial del programa, así como declaraciones no verificables recibidas del desarrollador, se transfieren al programa de prueba automática. GNATprove utiliza la plataforma Why3 [13] y los sistemas de prueba CVC4, Z3 y Alt-Ergo [14] . Los sistemas de terceros como Coq [14] también se pueden usar como prueba .
La primera versión de SPARK (basada en Ada 83) fue creada en la Universidad de Southampton con el apoyo del Ministerio de Defensa británico por Bernard Carré y Trevor Jennings , autores del confiable sistema de programación Pascal SPADE-Pascal [15] . Además, las siguientes empresas trabajaron en la mejora del lenguaje: Program Validation Limited, Praxis Critical Systems Limited (en adelante, Altran-Praxis, Altran) y AdaCore.
A principios de 2009, Praxis firmó un acuerdo con AdaCore y lanzó SPARK Pro bajo los términos de la GPL [16] . Luego, en junio de 2009, se lanzó la edición SPARK GPL, destinada al desarrollo de software libre y académico.
El lanzamiento de la versión de lenguaje de segunda generación SPARK 2014 se anunció el 30 de abril de 2014 [17] .
Comentarios
Fuentes