Diferencia entre revisiones de «Spark»
(Página creada con '{{Ficha_Software |nombre=SPARK |imagen= |descripción= Es un lenguaje de programación especialmente diseñado para sistemas de alta integridad. |creador= Bernard Carré y Trev...') |
|||
| Línea 12: | Línea 12: | ||
|licencia=[[Ada]] | |licencia=[[Ada]] | ||
|web=http://www.sparkada.com | |web=http://www.sparkada.com | ||
| − | }}<div align="justify">'''SPARK | + | }} |
| + | <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á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]]. | ||
==Ejemplo de código SPARK== | ==Ejemplo de código SPARK== | ||
| − | + | 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; | |
| − | + | isbegin | |
| − | + | Spark_IO.Put_Line (Spark_IO.Standard_Output, "Hola Mundo!", 0);end Hola_Mundo; | |
==Fuente == | ==Fuente == | ||
| − | |||
* [http://www.sparkada.com Página oficial de SPARK] | * [http://www.sparkada.com Página oficial de SPARK] | ||
* [http://www.prakis-his.com Praxis High Integrity Systems, Inc] | * [http://www.prakis-his.com Praxis High Integrity Systems, Inc] | ||
última versión al 12:49 4 dic 2013
| ||||||||||||
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.
Ejemplo de código SPARK
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; isbegin Spark_IO.Put_Line (Spark_IO.Standard_Output, "Hola Mundo!", 0);end Hola_Mundo;
