Diferencia entre revisiones de «Lenguaje de Programación SPARK»
(→Ejemplo) |
m |
||
| Línea 6: | Línea 6: | ||
}} | }} | ||
<div align="justify"> | <div align="justify"> | ||
| − | + | ||
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álisis de flujo de datos y de información. | 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álisis de flujo de datos y de información. | ||
| + | |||
== Historia== | == Historia== | ||
| + | |||
Los orígenes de este lenguaje de programación se encuentran en los trabajos realizados en la Universidad de Southamton (Reino Unido) sobre verificación formal de programas, y más concretamente en el desarrollo de SPADE (Southampton 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». | Los orígenes de este lenguaje de programación se encuentran en los trabajos realizados en la Universidad de Southamton (Reino Unido) sobre verificación formal de programas, y más concretamente en el desarrollo de SPADE (Southampton 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 Universidad con el patrocinio del Ministerio de Defensa (MoD) británico. Más tarde siguió siendo desarrollado por la empresa Program Validaton Limited (fundada por el profesor Carré), y después por Praxis Critical Systems Limited. En octubre de [[2004]] esta empresa se fusionó con High Integrity Systems Limited para formar Praxis High Integrity Systems. | La primera versión de SPARK estaba basada en Ada 83 y fue desarrollada en [[1988]] por Bernard Carré y Trevor Jennings en dicha Universidad con el patrocinio del Ministerio de Defensa (MoD) británico. Más tarde siguió siendo desarrollado por la empresa Program Validaton Limited (fundada por el profesor Carré), y después por Praxis Critical Systems Limited. En octubre de [[2004]] esta empresa se fusionó con High Integrity Systems Limited para formar Praxis High Integrity Systems. | ||
==Ejemplo== | ==Ejemplo== | ||
| Línea 16: | Línea 19: | ||
with Spark_IO; | with Spark_IO; | ||
| − | --# inherit Spark_IO; | + | --# inherit Spark_IO; |
--# main_program; | --# main_program; | ||
| + | |||
procedure Hola_Mundo | procedure Hola_Mundo | ||
| − | --# global in out Spark_IO.Outputs; | + | --# global in out Spark_IO.Outputs; |
| − | --# derives Spark_IO.Outputs from Spark_IO.Outputs; | + | --# derives Spark_IO.Outputs from Spark_IO.Outputs; |
is | is | ||
| + | |||
begin | begin | ||
| + | |||
Spark_IO.Put_Line (Spark_IO.Standard_Output, "Hola Mundo!", 0); | Spark_IO.Put_Line (Spark_IO.Standard_Output, "Hola Mundo!", 0); | ||
| + | |||
end Hola_Mundo; | end Hola_Mundo; | ||
| Línea 29: | Línea 36: | ||
*[http://www.sparkada.com/ Página oficial de SPARK] | *[http://www.sparkada.com/ Página oficial de SPARK] | ||
*[http://www.praxis-his.com/ Praxis High Integrity Systems] | *[http://www.praxis-his.com/ Praxis High Integrity Systems] | ||
| + | |||
==Hojas de referencia rápida del lenguaje== | ==Hojas de referencia rápida del lenguaje== | ||
*[http://www.praxis-his.com/sparkada/pdfs/SPARK_QRG1.pdf Hoja de referencia 1: Toolset and Annontations] | *[http://www.praxis-his.com/sparkada/pdfs/SPARK_QRG1.pdf Hoja de referencia 1: Toolset and Annontations] | ||
Revisión del 11:45 14 ene 2011
| ||||
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álisis de flujo de datos y de información.
Historia
Los orígenes de este lenguaje de programación se encuentran en los trabajos realizados en la Universidad de Southamton (Reino Unido) sobre verificación formal de programas, y más concretamente en el desarrollo de SPADE (Southampton 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 Universidad con el patrocinio del Ministerio de Defensa (MoD) británico. Más tarde siguió siendo desarrollado por la empresa Program Validaton Limited (fundada por el profesor Carré), y después por Praxis Critical Systems Limited. En octubre de 2004 esta empresa se fusionó con High Integrity Systems Limited para formar Praxis High Integrity Systems.
Ejemplo
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;
