We recently added a new section in the SPARK User's Guide called 'How to Write Subprograms Contracts'. This section explains which contracts are required for which verification. Although GNATprove can analyze a program without any contracts, the results may not be correct or precise depending on the verification objective:
- data dependencies and flow dependencies generated by GNATprove are safe over-approximations, so they may lead to false alarms when analyzing callers;
- imported subprograms (say, from C) require correct data dependencies, otherwise GNATprove incorrectly assumes that their contract is null (no global variables read or written);
- imported subprograms also require a correct precondition, otherwise GNATprove incorrectly assumes that their precondition is True (no constraints on the calling context);
- preconditions and postconditions should be precise enough to allow automatic verification of each subprogram considered separately, either to show program integrity or functional correctness.
The section is divided in 5 subsections on:
- generation of dependency contracts;
- writing contracts for program integrity;
- writing contracts for functional correctness;
- writing contracts on imported subprograms; and
- contextual analysis of subprograms without contracts.
Each section is rich of many examples, and we show and explain the results of running GNATprove on these examples.
See the User's Guide for more details, and let us know what you think!