H ? « ‹ ← → › »

Language peer sets for SPARK:
United Kingdom↑
United Kingdom/1990↑
Designed 1990 ↑
1990s languages ↑
Fifth generation↑
Post-Cold War↑
Multi-purpose ↑
Multi-purpose/1990↑
Multi-purpose/uk ↑

SPARK(ID:2518/spa010)

Provable Ada 

alternate simple view
Country: United Kingdom
Designed 1990
Published: 1990
Sammet category: Multi-purpose

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:
  • (1990) "SPARK An Annotated Ada Subset for Safety-Critical Programming", Tri-Ada '90.
  • (1999) "SPARK — The SPADE Ada Kernel" Praxis Critical Systems Limited, 1999. Abstract
  • (1999) "SPARK95 — The SPADE Ada 95 Kernel" Praxis Critical Systems Limited, 1999. Abstract
  • Chapman, Roderick and Dewar, Robert (1999) Chapman, Roderick and Dewar, Robert "Re-engineering a safety-critical system with SPARK95 and GNORT" Abstract pdf
          in (1999) Reliable Software Technologies - Ada-Europe '99 LNCS 1622 1999
  • King, Steve; Hammond, Jonathan; Chapman,Rod and A (1999) King, Steve; Hammond, Jonathan; Chapman,Rod and Andy Pryor "Is Proof More Cost Effective Than Testing?" Abstract pdf
          in (1999) IEEE Transactions on Software Engineering 26(8)
  • Dr. Roderick Chapman (2000) Dr. Roderick Chapman "Industrial Experience with SPARK" Praxis Critical Systems Limted, Presented at ACM SigAda 2000 conference Abstract pdf
          in (1999) IEEE Transactions on Software Engineering 26(8)
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder