SPARK

Es un subconjunto anotado de Ada desarrollado por la empresa británica Praxis High Integrity Systems, Inc Archivado el 10 de julio de 2006 en Wayback Machine.

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.

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