Anonymous user
Encyclopedia:SPARK Proof process: Difference between revisions
m
→Proving Verification Conditions: Ada -> link to Ada
(Added SPARK Proof Process page to the Encyclopedia) |
m (→Proving Verification Conditions: Ada -> link to Ada) |
||
Line 22:
An unproven verification condition may be unprovable, or may be provable but requiring more complex proof strategies than the Simplifier has available.
An '''unprovable''' verification condition may indicate a failure of the [[Ada]] code to satisfy the required property. If this is the case then the [[Ada]] code of the program must be modified to remove that failure.
An unprovable verification condition where there is no failure in the [[Ada]] code will be caused by the Examiner having insufficient information about the program state at the point that the verification condition is generated. This can be resolved by adding further annotations that make the required information available to the Examiner where it is required. Subsequent reanalysis should result in the verification conditions becoming provable.
If a verification condition is '''provable''' but not proved by the Simplifier then there are a range of possibilities open to the analyst.
| |||