| SPARK
Proofs |
|
|
|
|
|
|
|
|
|
|
| • | Optional
Annotations |
||||||||
| – | pre:
specifies the precondition of a procedure |
||||||||
| – | post:
specifies the postcondition of a procedure |
||||||||
| – | assert:
specifies loop invariants |
||||||||
| – | return:
defines the result of a function |
||||||||
