| 1234567891011121314151617181920212223242526272829303132 |
- .. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
- .. Copyright © 2019 Ariadne Devos
- Specifying and proving programs
- ===============================
- For formally proving programs correct, annotations in ACSL
- are interwoven with the source code, which can be fed into
- Frama-C for submission to automatic theorem provers.
- A specification of ACSL is available on https://frama-c.com,
- as is the free-software Frama-C platform (both GUI and CUI).
- A few guidelines are given.
- Contracts
- ---------
- The contract of a function is given where it is declared:
- the header file for exported functions. If a proposition
- is conditional on presence or absence of :ref:`speculation <speculation>`,
- this is modelled as being conditional on `S` or `NS` respectively,
- defined in `<sHT/nospec.h> `.
- Lemmas
- ------
- Invariants' names are suffixed by `I`, before any speculation suffix.
- Loops
- -----
- Specify relevant invariants, the frame (`assigns:`) and `variant:`
- for proving termination (if applicable). Frama-C cannot guess
- the invariants or the frame, and typically has little trouble
- proving them, but only if they are correct.
|
