Frozen: C++L 1.0.0. A change to this text needs an RFC and a new version
(STATUS.md, "V1 closure: stability").
This is the normative concrete grammar referenced by SPEC.md.
RFC 0015 reconciles earlier spellings.
Ordinary C++ categories below retain the selected C++ grammar and Clang semantics.
EBNF uses quoted tokens, [] for optional parts, {} for repetition and |
for alternatives. Whitespace separates tokens; canonical layout is section 49.
law, proof, proves, pure, verified, ghost, unsafe, trusted, type,
where, expects, ensures, decreases, invariant, forall, and exists
are contextual words. refl, exact, apply, assume, rewrite,
contradiction, cases, decompose, and induction are contextual proof
statements; contradiction, cases and decompose also begin a statement in a
verified function's body where the translation unit gives the word no other
meaning (sections 5.6 and 5.7), which a unit that imports a module cannot show
(SPEC.md WORD-019). omit
and by have meaning only in a case omission (section 5.7),
and omit begins one only where a case label followed by by comes after it.
result, old, and self have only the scopes defined below. C++ keywords take
precedence; case remains a runtime switch label. None of these additions
globally reserves an ordinary C++ identifier. A word immediately followed by
:: is the first component of a C++ nested-name-specifier and begins no C++L
construct (SPEC.md WORD-014): pure::inner g(); returns pure::inner, and
ghost::T g; declares a local.
cppl-declaration ::= law-declaration | proof-declaration
| refinement-type-declaration | ghost-declaration
| cppl-function-declaration | unsafe-declarationlaw-declaration ::= "law" identifier "(" [parameter-declaration-list] ")"
[expects-clause] proves-clause (";" | proof-body)
| "trusted" "law" identifier "(" [parameter-declaration-list] ")"
[expects-clause] proves-clause ";"
proves-clause ::= "proves" "(" specification-expression ")"A Law has one theorem conclusion, no runtime result, and at most one premise.
ensures is invalid on a Law. A semicolon requests automatic proof; failure
is a compilation error. A body supplies explicit proof steps. Neither introduces
an axiom. Only the explicit trusted law form introduces an assumption.
law zero_identity(unsigned x)
proves (x + 0u == x);
law given_zero(unsigned x)
expects (x == 0u)
proves (x == 0u)
{
assume h : x == 0u;
exact h;
}proof-declaration ::= "proof" identifier "(" [parameter-declaration-list] ")"
proves-clause proof-body
proof-body ::= "{" {proof-statement} "}"A proof names reusable evidence. Its body must close its goal. It has no runtime
representation. Parameters are universally quantified.
proof-statement ::= "refl" ";"
| "exact" evidence-reference ";"
| "apply" evidence-reference ";"
| "rewrite" evidence-reference ";"
| "assume" identifier ":" specification-expression ";"
| "contradiction" evidence-reference ";"
| cases-statement | decompose-statement | induction-statement
evidence-reference ::= qualified-id ["(" [argument-expression-list] ")"]In a proof body, an evidence reference names a premise bound by assume, a proof
declaration, or a trusted law (SPEC.md TRUSTED-006). A premise bound in the body
is the more local binding; a name that denotes more than one proof or trusted law
is refused (TRUSTED-009). In a verified function's body, the evidence of a
contradiction statement names a proof declaration only (§5.6).
refl; closes a definitionally reflexive equality. It cannot prove 1 == 2.
exact evidence; closes the goal with existing evidence of the required type.
Instantiation is written exact evidence(x);, never exact(evidence);.
apply evidence; applies established evidence and leaves its premises as goals.
assume h : P; names a premise supplied by the proof context. The stated
proposition must match that premise. It does not assert P or introduce trust.
The same form names Law premises, implication premises, case facts and induction
hypotheses. No arbitrary-proposition assume (P); form exists.
rewrite equality; uses checked equality evidence, left to right, to transform
the goal. The transformed goal must still be proven; a nonmatching rewrite fails.
contradiction evidence; closes the goal, whatever its shape, from evidence that
the context where it is written cannot occur. The named evidence must establish
an equality that cannot hold together with the premises standing there; it is
checked like any other evidence and introduces no trust of its own (SPEC
CASE-011, CASE-013). Evidence that rests on a trusted law carries that
dependency into the claim (TRUSTED-006). The same statement, written as the omit clause below, accounts for
an omitted case, which is a claim of its own and is reported as one (SPEC
CASE-012).
path-contradiction ::= "contradiction" evidence-reference ";"Written as a statement of a verified function's body, the same form claims that
no execution reaches it (SPEC VERIFIED-045). The facts established on the path
to it and the named evidence, whose arguments are read where the statement
stands, must contradict each other; the path ends there. It is ordinary C++
wherever the translation unit gives contradiction any other meaning, such as a
type, and in a function that is not verified it is ill-formed (SPEC
WORD-011). It erases to an empty statement: its ; stays (SPEC ERASE-016).
cases-statement ::= "cases" specification-expression "{" {proof-arm | case-omission} "}"
case-omission ::= "omit" proof-arm-label "by" "contradiction" evidence-reference ";"
decompose-statement ::= "decompose" specification-expression "{" proof-arm "}"Providers define states, discriminators and labels; the engine owns arms and
exhaustiveness. decompose uses components(bindings) for products. Bindings
are logical projections or aliases, never new runtime objects. The engine derives
a residual discriminator by negating named states. There is no wildcard and _
is not a proof catch-all. See SPEC section 20.
A case is covered by an arm or by an omit clause naming it, never by both and
never by the absence of both (SPEC CASE-004). omit states the claim at the
site where the label has meaning, and its evidence is checked under that case's
own discriminator premise, exactly as an arm's body would be. The engine never
searches the surrounding context to decide that a missing arm was intentional
(SPEC CASE-005). A case omission has no binders, because it has no body to
bind them in.
Written as a statement of a verified function's body, either statement splits
the rest of the path by the states of its subject's value where it is written
(SPEC CASE-017). Each arm continues the path with its case's facts; it holds
only nested cases or decompose statements and a contradiction claim that
ends its path, because there is no goal on a path for anything else to close
(SPEC CASE-019). A later write, aliased write, call effect or loop gives the
subject's storage a new version that no earlier case fact describes (SPEC
CASE-020). It is ordinary C++ wherever the translation unit gives the word any
other meaning, and ill-formed in a function that is not verified (SPEC
WORD-012). It erases to an empty statement (SPEC ERASE-016).
induction-statement ::= "induction" identifier ";"
| "induction" identifier "{" proof-arm {proof-arm} "}"The short form requests automation for every case. Explicit arms use the
settled domain labels, including zero and successor(pred) for unsigned
machine induction. The principle supplies its range premise and induction
hypothesis; assume names them. A domain needs a well-founded principle.
proof-arm ::= proof-arm-label ["(" proof-binder-list ")"] "=>" proof-body
proof-arm-label ::= id-expression | "alternative" "<" integer-literal ">"
proof-binder-list ::= identifier {"," identifier}This grammar is shared by every representation and by induction. The provider
controls binder arity and label meaning. Arm bodies may nest. Because a label is
an id-expression, any part of its qualification may carry template arguments,
as Machine<int>::Mode::on does for an enumerator of a class template's member
enumeration.
cppl-function-declaration ::= cpp-prefix-specifiers ["verified"] ["pure"]
cpp-function-declarator
[expects-clause] [ensures-clause] [decreases-clause]
cpp-function-body-or-semicolon
expects-clause ::= "expects" "(" specification-expression ")"
ensures-clause ::= "ensures" "(" specification-expression ")"Each kind occurs at most once and in the displayed order. A verified function
that returns a value states it with ensures, or returns a refinement type
whose predicate it owes; an expects-only verified function is therefore void.
It still incurs body safety obligations. No postcondition means no additional
postcondition assertion; it does not waive those obligations.
Preserve ordinary C++ specifier order. Place C++L function modifiers after
ordinary prefix specifiers and before the return type, in verified pure order.
Examples: static verified int, inline verified pure int,
constexpr verified pure int, consteval verified pure int,
virtual verified int. C++ restrictions on combinations still apply.
ghost prefixes a local declaration; trusted prefixes law; unsafe
prefixes a function declaration. These are not interchangeable function flags.
A modifier is one only where a return type follows it (SPEC.md WORD-015):
verified const int f() is verified, while verified const c{};,
verified static s; and verified operator*(verified, verified) use a type
named verified.
verified requests discharge of the function's contract and required body
obligations. It does not change runtime representation, linkage or ABI.
pure requests checked referential transparency. Legal forms are pure free and
member functions and verified pure functions. It permits neither observable
mutation nor unmodeled effects. Purity alone does not prove termination.
expects (P) is a caller precondition on functions and a theorem premise on Laws.
Use one predicate, for example expects (amount >= 0 && amount <= balance).
ensures (Q) applies only to runtime functions and describes normal return.
Use one predicate; combine independent conditions with &&.
The return-value identifier exists only in non-void function postconditions.
It has no special meaning in Laws, preconditions, refinements or runtime bodies.
An ordinary C++ declaration named result remains valid outside that context.
A void postcondition cannot refer to a return value.
old-expression ::= "old" "(" specification-expression ")"old(expression) denotes the expression's function-entry value in a function
postcondition. It does not copy a runtime object. The entry expression must be
well-defined and specification-visible. result and nested old are not
entry values. Elsewhere old is an ordinary C++ name, not a snapshot form.
refinement-type-declaration ::= "type" identifier
["(" formal-index-parameter-list ")"]
"=" type-id "where" "(" specification-expression ")" ";"type NonNegative = int where (self >= 0);
type Percentage = NonNegative where (self <= 100);The predicate remains attached to the declaration. Refinement identity is
verification-level; the runtime representation is its base C++ type. where
follows the base type directly: after , or an operator no type-id ends in it
is ordinary C++, and type a = 5, where (6); declares two variables
(SPEC.md WORD-016).
self denotes the candidate value only in a refinement predicate. Member
contracts use ordinary member lookup and this; they introduce no second
meaning for self. Outside refinements it is an ordinary C++ identifier.
formal-index-parameter-list ::= parameter-declaration {"," parameter-declaration}
refinement-application ::= qualified-id "<" argument-expression-list ">"type Index(std::size_t n) = std::size_t where (self < n);Index declarations are typed; applications use Index<4>. Indices are in scope
in the predicate. There is no alternate untyped index or call-style application.
Dependent names and template substitution use Clang's ordinary C++ rules.
validation-expression ::= "validate" "<" identifier ">" "(" expression ")"if (validate<Positive>(raw)) {
Positive p = raw;
}The identifier is the name a refinement declaration without indices gives its
type; the expression has that refinement's base type, and the validation has
type bool (SPEC.md RUNTIMECHECK-018). It is runtime code: it stands only in
the body of a verified function, outside every unsafe block, and never in a
contract clause, loop clause, Law, proof or refinement predicate
(RUNTIMECHECK-019). Where the translation unit declares or uses validate for
anything else, the spelling is ordinary C++ (SPEC.md WORD-013).
Use ordinary C++ enums, classes, structs and standard-library types. C++L introduces no second algebraic data declaration or template system.
| Representation | Labels |
|---|---|
| Scoped enum | Qualified enumerators and unnamed(value) |
std::variant |
alternative<I>(payload) and valueless |
std::optional |
some(payload) and none |
std::expected |
value(payload) and error(payload) |
| Pointer | null and non_null(value) |
| Product | components(first, second) with the representation's arity |
Aliases use canonical Clang type identity. Non-null does not prove a memory
capability. unnamed and valueless are real residual states, not wildcards.
Providers model public value semantics, never library layout. A newly added state must invalidate stale exhaustiveness evidence.
mathematical-domain ::= "@N" | "@Z"
| "@Seq" "<" verification-type ">"
| "@Set" "<" verification-type ">"
| "@Map" "<" verification-type "," verification-type ">"
verification-type ::= type-id | mathematical-domainThese established names denote proof-only domains. They may occur in Law/proof
parameters, quantifier binders and ghost locals, never runtime storage or ABI.
C++ int remains a machine integer.
ghost-declaration ::= "ghost" simple-declarationOnly locals in verification-enabled blocks are legal. No ghost member, runtime
parameter or global is implied. Initializers must be specification-safe;
runtime computation, lifetime and effects cannot depend on erased state.
Where the unit uses ghost as a C++ name, the declaration is ordinary C++, with
a warning only in a verified body (SPEC.md WORD-018).
unsafe-statement ::= "unsafe" compound-statementThe body executes as ordinary C++. Its unproved safety is explicit and cannot
manufacture evidence. Where the unit uses unsafe as a C++ name, unsafe {...}
is ordinary C++, with a warning only in a verified body or where the braces hold
a statement (SPEC.md WORD-018).
unsafe-declaration ::= cpp-prefix-specifiers "unsafe" cpp-function-declarationThis marks an unverified operation boundary. It is not trusted, cannot be
combined with verified or pure to bypass checks, and has no expression form.
Only trusted law is a trusted declaration. It always ends with ;, never a
proof body. The assumption and its dependent evidence retain trust provenance.
A proof statement uses one by naming it as evidence (§5); nothing else does.
loop-clauses ::= [invariant-clause] [decreases-clause]
invariant-clause ::= "invariant" "(" specification-expression ")"
cppl-while-statement ::= "while" "(" condition ")" loop-clauses compound-statementOne invariant must hold on entry and be preserved by every continuing iteration.
decreases additionally requests termination evidence.
An invariant is a condition, or an implication, an equivalence, a conjunction or a disjunction of conditions (§29, §30); a quantifier, formal equality and a memory capability are not read in an invariant by this implementation.
One clause whose parentheses hold a declarator, before braces that hold no
statement and are followed by ; or ,, is the C++ declaration it also spells
(SPEC.md WORD-016): while (n-- > 0) decreases (k) {n}; declares k. A loop
meant there is written with a statement in its body or without the ;.
cppl-for-statement ::= cpp-for-header loop-clauses compound-statement
cppl-range-for-statement ::= cpp-range-for-header loop-clauses compound-statement
cppl-do-statement ::= "do" loop-clauses compound-statement "while" "(" expression ")" ";"Clauses follow the loop header. For do, the header is do; the trailing
while remains ordinary C++ syntax. Clause scopes follow the underlying loop's
C++ bindings; they cannot refer to body locals before those locals exist.
decreases-clause ::= "decreases" "(" specification-expression-list ")"
specification-expression-list ::= specification-expression {"," specification-expression}One or more measures form a lexicographic well-founded order. Presence of the clause requests proof of strict descent on recursive calls/continuing iterations. Proof-producing computation must terminate independently of whether a clause is written. Runtime verification without a requested termination property establishes partial correctness. A failed requested termination proof is an error.
forall-expression ::= "forall" "(" parameter-declaration-list ")"
"{" specification-expression "}"
exists-expression ::= "exists" "(" parameter-declaration-list ")"
"{" specification-expression "}"Quantifiers are specification-only. Binder types and names are Clang-resolved.
P -> Q is right-associative formal implication in specification context.
Parenthesize C++ pointer member access there so it retains its C++ meaning.
A parenthesized group in a proposition is that member access when it holds
exactly one: an operand, its postfix operators with at least one -> naming a
member, and only prefix operators before it ((p->m), (!p->ready)). Any other
parenthesized group is a proposition, its top-level -> an implication, so a
conjunction of implications is written (a == 0 -> r == 0) && (a > 0 -> r > 0)
(§33). (a -> b) with a name on each side is member access; an implication
between two names is written with a comparison on a side, (a -> b == true), or
as !a || b.
P <-> Q means (P -> Q) && (Q -> P) in specification context.
formal-equality-expression ::= "Eq" "<" type-id ">"
"(" specification-expression "," specification-expression ")"Eq<T>(a, b) is a formal proposition, not a fabricated runtime C++ template.
C++ a == b retains its Boolean semantics.
Specification expressions extend side-effect-free modeled C++ expressions with
quantifiers, formal equality, implication, equivalence and contextual old.
Unsupported semantics are errors, never implicit assumptions.
From tightest to loosest: ordinary C++ operators above &&, then &&, ||,
->, <->. Use parentheses to make mixed formal/C++ structure explicit.
References resolve in the proof context to established evidence. Spelling or successful C++ compilation alone never supplies evidence.
A function entity has one logical contract. Put public contracts on header declarations; the matching definition inherits that contract. Repeated identical contracts are permitted, conflicting ones are errors. The formatter never copies contracts from declarations onto definitions.
Laws, proofs and refinements have namespace or class scope. Translation-unit helpers belong in an unnamed namespace. Block-local Law declarations are not a second declaration form. Ghost declarations have block scope; unsafe blocks have statement scope. Function contracts follow ordinary declaration scopes.
The implicit object follows ordinary C++ member lookup and constness rules. It is part of the quantified specification context, never a runtime theorem object.
Member contracts follow the complete declarator. this and unqualified members
retain C++ meaning. A constructor has no result; its postcondition describes
the initialized object. Entry snapshots cannot read uninitialized subobjects.
A constructor's clauses precede its :; the mem-initializers after it belong to
the body, so explicit S(int a) : expects(a) {} initializes a member
(SPEC.md WORD-017).
C++ owns template syntax, lookup and substitution. Contract/refinement/proof metadata must remain visible at verification of each specialization.
Ordinary attributes keep their C++ placement. C++L never moves an attribute to another entity while canonicalizing modifiers.
Storage, linkage, inline, constexpr, consteval, and virtual retain C++
meaning. Section 7 defines only the placement of the added C++L modifiers.
noexcept remains in the ordinary declarator, before specification clauses.
Postconditions describe normal returns, not an invented exception model.
A trailing return type precedes specification clauses; C++L does not split the
ordinary declarator. The type is named first: a clause word that begins it is
the type, as in auto pick() -> ensures (&)[3] (SPEC.md WORD-017).
const, reference qualifiers, override, and final keep their C++ positions,
before the specification clauses.
Ordinary declarator, then C++L clauses, then body or semicolon. Ordinary runtime bodies continue to be parsed by Clang.
Law names occupy a formal namespace associated with C++ scope and produce no
runtime callable symbol. Ordinary C++ lookup never finds one; only a Law's or
a proof's proposition names a Law (SPEC.md LAW-008). Ambiguous references
are errors.
Proof names identify evidence in that formal scope, with no runtime symbol.
Bodyless declarations and primitive proof commands end with ;. Proof/Law
bodies and decomposition/induction arms end with } and no extra semicolon.
The short induction statement ends with ;.
Use the shared cppl-format engine through CLI, LSP or CI. Clauses require one
space before (, occur on continuation lines, and use one clause of each kind
in grammar order. A contracted body's { is on the next line at declaration
indentation. Other braces follow .clang-format. Proof arms are expanded,
with label(bindings) => { and one blank line between arms. A case omission is
one line, omit label by contradiction evidence;, separated from its neighbours
the same way, with the statement after by kept as written. A comment between
arms keeps its place: one on the line of the {, } or ; before it stays on
that line, and one on a line of its own stays on its own line, before the arm
that follows or before the block's closing }. A case split in a verified body
is a statement of that body: its keyword starts a line at the statement's
indentation, one level deeper as the unbraced body of if, else, while,
for or do, its arms follow the same rules, and the statement after its
closing } starts a line of its own. where stays on the
refinement declaration subject to normal ColumnLimit wrapping. Predicates use
the same indentation and line-width configuration as C++ expressions.
Law ensures, parenthesis-free clauses, repeated clause kinds, function proves,
proof case, wildcard _, call-style proof commands, untyped refinement indices,
and pure verified are noncanonical/illegal forms. Migration tools may offer
an explicit semantics-preserving fix; the compiler accepts no legacy dialect.
DEVELOPER_GUIDE.md supplies practical examples. Tests and formatter checks maintain their agreement with this grammar.
| Region | Authority |
|---|---|
| Ordinary declarations, templates and runtime bodies | C++ and Clang |
| Contracts and refinement predicates | C++L grammar and SPEC |
| Proof declarations, statements and arms | C++L grammar and SPEC |
| Canonical presentation | Shared C++L formatter plus clang-format |
A contextual addition must never reinterpret valid supported C++. No spelling in historical RFCs overrides this grammar. Verification limitations do not introduce alternative syntax or permission to accept unchecked proof evidence.