SPARK(ID:2518/spa010)

Provable Ada 

Southampton University and Program Validation, Ltd. An annotated subset of Ada 83 for formal verification. Eliminates derived types, anonymous types, access types, variant records, recursion, generics, tasking and exceptions.

"It includes Ada constructs regarded as essential for the construction of complex software, such as packages, private types, typed constants, functions with structured values, and the library system. It excludes tasks, exceptions, generic units, access types, use clauses, type aliasing, anonymous types, default values in record declarations, default subprogram parameters, goto statements, and declare statements. " from Spark Design Philosophy
Related languages
Ada 83 => SPARK   Subset
SPARK => SAL   Augmentation of
SPARK => SPARK95   Evolution of
References:
  • "SPARK An Annotated Ada Subset for Safety-Critical Programming", Tri-Ada '90. view details
  • "SPARK — The SPADE Ada Kernel" Praxis Critical Systems Limited, 1999. view details Abstract: This paper defines SPARK, an annotated subset of the Ada 83 language. It describes the differences between SPARK and Ada and also defines the SPARK syntax.
  • "SPARK95 — The SPADE Ada 95 Kernel" Praxis Critical Systems Limited, 1999. view details Abstract: This paper defines SPARK 95, an annotated subset of the Ada 95 language. It describes the differences between SPARK 95 and Ada 95 and defines the SPARK 95 syntax.
  • Chapman, Roderick and Dewar, Robert "Re-engineering a safety-critical system with SPARK95 and GNORT" view details Abstract: A paper about porting the SHOLIS project software to SPARK95 using ACT's GNAT-No-Runtime (GNORT) technology. This paper was presented at the 1999 Ada Europe conference, and went on to win the conference prize for best presentation. pdf
          in Reliable Software Technologies - Ada-Europe '99 LNCS 1622 1999 view details
  • King, Steve; Hammond, Jonathan; Chapman,Rod and Andy Pryor "Is Proof More Cost Effective Than Testing?" view details Abstract: A paper, originally appearing in 1999 World Congress on Formal Methods, but re-published in IEEE Transactions on Software Engineering. Considers the use of Z, SPARK and Proof in the SHOLIS project and compares the effectiveness of proof with other, more traditional verification activities. pdf
          in IEEE Transactions on Software Engineering 26(8) view details
  • Dr. Roderick Chapman "Industrial Experience with SPARK" Praxis Critical Systems Limted, Presented at ACM SigAda 2000 conference view details Abstract: This paper discusses three large, real-world projects (C130J, SHOLIS and the MULTOS CA) where SPARK has made a contribution to meeting stringent software engineering standards. pdf
          in IEEE Transactions on Software Engineering 26(8) view details