SPARK Reference Manual
25.0w
1. Introduction
2. Lexical Elements
3. Declarations and Types
4. Names and Expressions
5. Statements
6. Subprograms
7. Packages
8. Visibility Rules
9. Tasks and Synchronization
10. Program Structure and Compilation Issues
11. Exceptions
12. Generic Units
13. Representation Issues
14. Predefined Language Environment (Annex A)
15. Language-Defined Aspects and Attributes (Annex K)
16. Language-Defined Pragmas (Annex L)
17. Glossary
A. SPARK 2005 to SPARK 2014 Mapping Specification
B. GNU Free Documentation License
SPARK Reference Manual
Index
Index
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
J
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
U
|
V
|
Y
A
Abstract_State
Access
access type
aliasing
allocating context
allocating function
Assert_And_Cut
assertion expression
Assume
Async_Readers
Async_Writers
asynchronous readers
asynchronous writers
B
borrowing traversal function
C
constant with variable inputs
in Global
Constant_After_Elaboration
in Global
constituent
constructive analysis
requirement
Contract_Cases
D
data-flow analysis
deallocation
Default_Initial_Condition
define full default initialization
Depends
E
Effective_Reads
Effective_Writes
effectively volatile
object
type
effectively volatile for reading
exclusion of predicates
object
type
elaboration
entire object
entity
executable contracts
executable semantics
expression function
expression with a variable input
disallowed contexts
Extensions_Visible
External
external state
F
flow analysis
formal verification
full default initialization
in allocators
G
generative analysis
requirement
Ghost
see ghost code
ghost code
Global
global item
goto
H
hidden state
I
immutable parameter
immutable stand-alone constant
information-flow analysis
Initial_Condition
and elaboration
initialization
by proof
of constituents
of package state
Initialized
Initializes
and elaboration
interfering object
Invariant
Iterable
J
Jorvik profile
L
Loop_Entry
Loop_Invariant
Loop_Variant
M
memory leak
for expressions
for objects
N
No_Caching
non-interfering context
for read of volatile object
O
observing traversal function
ownership
borrow
move
observe
P
Part_Of
in state refinement
of task or protected object
portability
order of evaluation and overflows
postcondition
potential aliases
potentially overlap
precondition
R
Ravenscar profile
reachable part
recursive subprograms
Refined_Depends
Refined_Global
Refined_Post
Refined_State
Relaxed_Initialization
retrospective analysis
root object
S
side effects
SPARK_Mode
state abstraction
state refinement
external state
subprogram input
subprogram output
subprogram with side effects
Subprogram_Variant
subtype predicate
T
tasking
termination
of Dynamic_Predicate
of loop
of subprogram
traversal function
Type_Invariant
U
Unchecked_Deallocation
V
verification condition
for Access on subprogram
for Dynamic_Predicate
for Initial_Condition
for Refined_Post
for run-time checks
for Type_Invariant
on dispatching operation
view of an entity
visible state
volatile function
Volatile_Function
see volatile function
Y
yield synchronized objects