| SPARK
Language |
|
|
|
|
|
|
|
|
|
|
|
|
| • | Subset
of Ada |
||||||||||
| – | Removed:
Gotos, aliasing, default parameters, |
||||||||||
| side
effects in functions, recursion, tasks, user- |
|||||||||||
| defined
exceptions, exception handlers, and |
|||||||||||
| generics. |
|||||||||||
| • | Precisely
defined – formal semantics |
||||||||||
| • | Require
data-flow annotations |
||||||||||
