CHISPA (lenguaje de programación)

CHISPA - CHISPEAR
clase de idioma paradigma múltiple
Apareció en 1988
Desarrollador Altran , AdaCore
Liberar 22 (2021 ) ( 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] .

Conceptos

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] .

Contratos y dependencias

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 ;

Verificación

Al verificar programas, se utilizan los siguientes métodos:

  • verificar el cumplimiento de las condiciones previas y posteriores de las funciones;
  • comprobar la ausencia de código capaz de lanzar una excepción ;
  • análisis de dependencia de transmisión, que comprueba la inicialización de las variables y la relación entre los parámetros y el resultado de las funciones.

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 .

Historia

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] .

Véase también

Notas

Comentarios

  1. A partir de 2020, solo un compilador (GNAT) es totalmente compatible con Ada 2012 y SPARK 2014 solo se puede usar con él.

Fuentes

  1. ↑ 1 2 3 4 SPARK - The SPADE Ada Kernel (incluido RavenSPARK) . docs.adacore.com . Consultado el 10 de octubre de 2020. Archivado desde el original el 7 de septiembre de 2021.
  2. ↑ 1 2 Certificación con SPARK . www.ada-ru.org . Consultado el 10 de octubre de 2020. Archivado desde el original el 13 de mayo de 2021.
  3. Johanes Kliemann. Programa de verificación con SPARK - Cuando tu código no debe fallar (2018). Consultado el 10 de octubre de 2020. Archivado desde el original el 16 de mayo de 2021.
  4. Eurofighter Typhoon - Proyectos de clientes - AdaCore . www.adacore.com . Consultado el 10 de octubre de 2020. Archivado desde el original el 21 de septiembre de 2020.
  5. Avión Be-200 . www.ada-ru.org . Consultado el 10 de octubre de 2020. Archivado desde el original el 13 de mayo de 2021.
  6. ↑ ¿Se eligió GNAT Pro para  el sistema ATC de próxima generación  del Reino Unido ? . AdaCore . Consultado el 10 de octubre de 2020. Archivado desde el original el 21 de septiembre de 2020.
  7. Espacio-AdaCore . www.adacore.com . Consultado el 10 de octubre de 2020. Archivado desde el original el 21 de octubre de 2020.
  8. Práctico . La criptografía Skein derivada de Ada muestra SPARK , SD Times , BZ Media LLC (24 de agosto de 2010). Archivado desde el original el 25 de agosto de 2010. Consultado el 31 de agosto de 2010.
  9. David Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens. Un sistema multidominio basado en hardware de alto rendimiento y seguridad  //  Seguridad informática, confiabilidad y protección / Amund Skavhaug, Jérémie Guiochet, Friedemann Bitsch. - Cham: Springer International Publishing, 2016. - P. 102–113 . - ISBN 978-3-319-45477-1 . -doi : 10.1007 / 978-3-319-45477-1_9 . Archivado desde el original el 20 de enero de 2022.
  10. Genode - Estructura del sistema operativo Genode . genode.org . Consultado el 10 de octubre de 2020. Archivado desde el original el 28 de octubre de 2020.
  11. Muen | SK para x86/64 . muen.sk._ _ Consultado el 10 de octubre de 2020. Archivado desde el original el 25 de octubre de 2020.
  12. Henry F. Ledgard, Andrew Singer. Reducción de Ada (o hacia un subconjunto estándar de Ada)  // Comunicaciones del ACM. - 1982-02-01. - T. 25 , n. 2 . — S. 121–125 . — ISSN 0001-0782 . -doi : 10.1145/ 358396.358402 .
  13. Por qué3 . por qué3.lri.fr._ Consultado el 10 de octubre de 2020. Archivado desde el original el 12 de octubre de 2020.
  14. ↑ 1 2 Probadores alternativos - Guía del usuario de SPARK 22.0w . docs.adacore.com . Consultado el 10 de octubre de 2020. Archivado desde el original el 12 de octubre de 2020.
  15. Bernard Carré. Programación confiable en lenguajes estándar  (inglés)  // Software de alta integridad / CT Sennett. — Boston, MA: Springer EE. UU., 1989. — P. 102–121 . - ISBN 978-1-4684-5775-9 . -doi : 10.1007 / 978-1-4684-5775-9_5 .
  16. Praxis y AdaCore anuncian SPARK  Pro . AdaCore . Consultado el 10 de octubre de 2020. Archivado desde el original el 21 de septiembre de 2020.
  17. Uso de SPARK en un  contexto de certificación . El Blog de AdaCore . Consultado el 10 de octubre de 2020. Archivado desde el original el 12 de octubre de 2020.

Literatura

Enlaces