SPARK (lenguaje de programación) - SPARK (programming language)

Este artículo trata sobre el lenguaje de programación . Para conocer el marco de trabajo de computación en clúster que se puede ejecutar en Scala , Java y Python , consulte Apache Spark .
CHISPA - CHISPEAR
Sparkada.jpg
Paradigma Multi-paradigma
Desarrollador Altran y AdaCore
Lanzamiento estable
Comunidad 2021/1 de junio de 2021 ; hace 4 meses ( 01/06/2021 )
Disciplina de mecanografía estático , fuerte , seguro , nominativo
SO Multiplataforma : Linux , Microsoft Windows , Mac OS X
Licencia GPLv3
Sitio web Sobre SPARK
Implementaciones importantes
SPARK Pro, SPARK GPL Edition, Comunidad SPARK
Influenciado por
Ada , Eiffel

SPARK es un lenguaje de programación de computadora formalmente definido basado en el lenguaje de programación Ada , destinado al desarrollo de software de alta integridad utilizado en sistemas donde es esencial una operación predecible y altamente confiable. Facilita el desarrollo de aplicaciones que exigen seguridad, protección o integridad empresarial.

Originalmente, había tres versiones del lenguaje SPARK (SPARK83, SPARK95, SPARK2005) basadas en Ada 83, Ada 95 y Ada 2005 respectivamente.

Una cuarta versión del lenguaje SPARK, SPARK 2014, basada en Ada 2012, fue lanzada el 30 de abril de 2014. SPARK 2014 es un rediseño completo del lenguaje y las herramientas de verificación de apoyo .

El lenguaje SPARK consiste en un subconjunto bien definido del lenguaje Ada que usa contratos para describir la especificación de componentes en una forma adecuada para la verificación tanto estática como dinámica.

En SPARK83 / 95/2005, los contratos están codificados en comentarios de Ada y, por lo tanto, son ignorados por cualquier compilador estándar de Ada, pero son procesados ​​por SPARK "Examiner" y sus herramientas asociadas.

SPARK 2014, por el contrario, utiliza la sintaxis de "aspecto" incorporada de Ada 2012 para expresar contratos, llevándolos al núcleo del lenguaje. La herramienta principal para SPARK 2014 (GNATprove) se basa en la infraestructura GNAT / GCC y reutiliza casi la totalidad del front-end de GNAT Ada 2012.

Resumen técnico

SPARK utiliza las fortalezas de Ada mientras intenta eliminar todas sus posibles ambigüedades y construcciones inseguras. Los programas SPARK están diseñados para ser inequívocos, y se requiere que su comportamiento no se vea afectado por la elección del compilador Ada . Estos objetivos se logran en parte omitiendo algunas de las características más problemáticas de Ada (como las tareas paralelas sin restricciones ) y en parte mediante la introducción de contratos que codifican las intenciones y requisitos del diseñador de aplicaciones para ciertos componentes de un programa.

La combinación de estos enfoques permite que SPARK cumpla con sus objetivos de diseño, que son:

  • solidez lógica
  • rigurosa definición formal
  • semántica simple
  • seguridad
  • poder expresivo
  • verificabilidad
  • requisitos de recursos limitados (espacio y tiempo).
  • requisitos mínimos del sistema de tiempo de ejecución

Ejemplos de contratos

Considere la especificación del subprograma Ada a continuación: 

procedure Increment (X : in out Counter_Type);

En Ada pura, esto podría incrementar la variable Xen uno o mil; o podría establecer algún contador global Xy devolver el valor original del contador en X; o puede que no haga absolutamente nada con él X.

Con SPARK 2014, los contratos se agregan al código para proporcionar información adicional sobre lo que realmente hace un subprograma. Por ejemplo, podemos modificar la especificación anterior para decir: 

procedure Increment (X : in out Counter_Type)
  with Global => null,
       Depends => (X => X);

Esto especifica que el Incrementprocedimiento no usa (ni actualiza ni lee) ninguna variable global y que el único elemento de datos usado para calcular el nuevo valor de Xes él Xmismo.

Alternativamente, el diseñador puede especificar: 

procedure Increment (X : in out Counter_Type)
  with Global  => (In_Out => Count),
       Depends => (Count  => (Count, X),
                   X      => null);

Esto especifica que Incrementusará la variable global Counten el mismo paquete que Increment, que el valor exportado de Countdepende de los valores importados de County X, y que el valor exportado de Xno depende de ninguna variable en absoluto y se derivará solo de datos constantes .

Si GNATprove se ejecuta luego en la especificación y el cuerpo correspondiente de un subprograma, analizará el cuerpo del subprograma para construir un modelo del flujo de información. Luego, este modelo se compara con el especificado por las anotaciones y cualquier discrepancia informada al usuario.

Estas especificaciones se pueden ampliar aún más afirmando varias propiedades que deben mantenerse cuando se llama a un subprograma ( condiciones previas ) o que se mantendrán una vez que se haya completado la ejecución del subprograma (condiciones posteriores ). Por ejemplo, podríamos decir lo siguiente: 

procedure Increment (X : in out Counter_Type)
  with Global  => null,
       Depends => (X => X),
       Pre     => X < Counter_Type'Last,
       Post    => X = X'Old + 1;

Esto, ahora, especifica no solo que Xse deriva solo de sí mismo, sino también que antes de que Incrementse llame Xdebe ser estrictamente menor que el último valor posible de su tipo y que luego Xserá igual al valor inicial de Xmás uno.

Condiciones de verificación

GNATprove también puede generar un conjunto de condiciones de verificación o VC. Estas condiciones se utilizan para establecer si ciertas propiedades son válidas para un subprograma determinado. Como mínimo, GNATprove generará VC para establecer que todos los errores de tiempo de ejecución no pueden ocurrir dentro de un subprograma, como:

  • índice de matriz fuera de rango
  • violación de rango de tipo
  • división por cero
  • desbordamiento numérico.

Si se agrega una condición posterior o cualquier otra afirmación a un subprograma, GNATprove también generará VC que requieren que el usuario muestre que estas propiedades son válidas para todas las rutas posibles a través del subprograma.

Bajo el capó, GNATprove utiliza el lenguaje intermedio Why3 y el generador de VC, y los probadores de teoremas CVC4, Z3 y Alt-Ergo para descargar VC. El uso de otros probadores (incluidos los verificadores de pruebas interactivos) también es posible a través de otros componentes del conjunto de herramientas Why3.

Historia

La primera versión de SPARK (basada en Ada 83) fue producida en la Universidad de Southampton (con el patrocinio del Ministerio de Defensa del Reino Unido ) por Bernard Carré y Trevor Jennings. El nombre SPARK se deriva de SPADE Ada Kernel , en referencia al subconjunto SPADE del lenguaje de programación Pascal .

Posteriormente, el lenguaje fue ampliado y perfeccionado progresivamente, primero por Program Validation Limited y luego por Praxis Critical Systems Limited. En 2004, Praxis Critical Systems Limited cambió su nombre a Praxis High Integrity Systems Limited. En enero de 2010, la empresa se convirtió en Altran Praxis .

A principios de 2009, Praxis se asoció con AdaCore y lanzó "SPARK Pro" bajo los términos de la GPL. A esto le siguió en junio de 2009 la SPARK GPL Edition 2009, dirigida a las comunidades académicas y de software libre .

En junio de 2010, Altran-Praxis anunció que el lenguaje de programación SPARK se utilizaría en el software del proyecto estadounidense Lunar CubeSat , que se espera esté terminado en 2015.

En enero de 2013, Altran-Praxis cambió su nombre a Altran.

La primera versión Pro de SPARK 2014 se anunció el 30 de abril de 2014, y fue seguida rápidamente por la edición SPARK 2014 GPL, dirigida a las comunidades académicas y de software libre .

Aplicaciones industriales

Sistemas relacionados con la seguridad

SPARK se ha utilizado en varios sistemas críticos de seguridad de alto perfil, que abarcan la aviación comercial ( motores a reacción de la serie Rolls-Royce Trent , el sistema ARINC ACAMS, el Lockheed Martin C130J), la aviación militar ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), aire -gestión del tráfico (sistema iFACTS NATS del Reino Unido), ferrocarril (numerosas aplicaciones de señalización), médico (el dispositivo de asistencia ventricular LifeFlow ) y aplicaciones espaciales (el proyecto CubeSat del Vermont Technical College ).

Sistemas relacionados con la seguridad

SPARK también se ha utilizado en el desarrollo de sistemas seguros. Los usuarios incluyen Rockwell Collins (soluciones de dominio cruzado Turnstile y SecureOne), el desarrollo del MULTOS CA original, el demostrador NSA Tokeneer, la estación de trabajo multinivel secunet, el kernel de separación Muen y el cifrador de dispositivo de bloque Genode.

En agosto de 2010, Rod Chapman, ingeniero principal de Altran Praxis, implementó Skein , uno de los candidatos para SHA-3 , en SPARK. Al comparar el rendimiento de las implementaciones de SPARK y C y después de una cuidadosa optimización, logró que la versión de SPARK se ejecutara solo entre un 5 y un 10% más lento que C. Mejora posterior del extremo medio de Ada en GCC (implementado por Eric Botcazou de AdaCore ) cerró la brecha, con el código SPARK coincidiendo exactamente con el C en rendimiento.

NVIDIA también ha adoptado SPARK para la implementación de firmware crítico para la seguridad.

En 2020, Rod Chapman volvió a implementar la biblioteca criptográfica TweetNaCl en SPARK 2014. La versión SPARK de la biblioteca tiene una prueba autoactiva completa de seguridad de tipos, seguridad de memoria y algunas propiedades de corrección, y conserva algoritmos de tiempo constante en todo momento. El código SPARK también es significativamente más rápido que TweetNaCl.

Ver también

Referencias

Otras lecturas

enlaces externos