SPARK

De Wikipedia, la enciclopedia libre
Saltar a: navegación, búsqueda

SPARK es un lenguaje de programación especialmente diseñado para sistemas de alta integridad. Es un subconjunto anotado de Ada desarrollado por la empresa británica Praxis High Integrity Systems, Inc que elimina ciertas características del lenguaje consideradas peligrosas en este tipo de sistemas (como las excepciones o la sobrecarga de operadores), y que añade anotaciones formales para realizar automáticamente análhampton Program Analysis Development Environment), un conjunto de herramientas destinadas al análisis de flujo de datos y de información. De hecho, el nombre «SPARK» deriva de «SPADE Ada Kernel».

La primera versión de SPARK estaba basada en Ada 83 y fue desarrollada en 1988 por Bernard Carré y Trevor Jennings en dicha

Ejemplo de código SPARK[editar]

El típico ejemplo de Hola mundo en SPARK es:

with Spark_IO;
--# inherit Spark_IO;
--# main_program;

procedure Hola_Mundo
--# global in out Spark_IO.Outputs;
--# derives Spark_IO.Outputs from Spark_IO.Outputs;
is
begin
   Spark_IO.Put_Line (Spark_IO.Standard_Output, "Hola Mundo!", 0);
end Hola_Mundo;

Enlaces relacionados[editar]

Enlaces externos[editar]