Language reference

Compact lookup for contract syntax and semantics. For a guided introduction, start with The CppVerify Book; for backends and cpp-verify flags, see Chapter 17 — Backends, modular calls, and debugging and Commands and flags.

Examples on these pages write the constructs through the alias cv and use the names of <cppverify.h> (valid, seq, set, multiset, map, …) unqualified, as a file does after:

namespace cv = cppverify;
using namespace cppverify;

<cppverify.h> itself needs no #include (see Contract syntax).

Every complete example is compiled and verified by the test suite (website/scripts/check-doc-examples.py), and where a page shows verdicts, the example must give them. A few snippets that are part of a larger program, such as the layout of a loop’s clauses, are not run.

• Contract syntax
• Contract expressions
• Functions and loops
• Ghost, spec, and proofs
• Structs and type invariants
• Pointers
• Dynamic storage
• Integers
• Commands and flags
• Current limitations and C++ readiness