56 lines
2.6 KiB
Markdown
56 lines
2.6 KiB
Markdown
[basic.contract.general]
|
||
|
||
# 6 Basics [[basic]](./#basic)
|
||
|
||
## 6.11 Contract assertions [[basic.contract]](basic.contract#general)
|
||
|
||
### 6.11.1 General [basic.contract.general]
|
||
|
||
[1](#1)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7567)
|
||
|
||
[*Contract assertions*](#def:contract_assertion "6.11.1 General [basic.contract.general]") allow the programmer to specify
|
||
properties of the state of the program
|
||
that are expected to hold at
|
||
certain points during execution[.](#1.sentence-1)
|
||
|
||
Contract assertions are introduced by[*precondition-specifier*](dcl.contract.func#nt:precondition-specifier "9.4.1 General [dcl.contract.func]")*s*,[*postcondition-specifier*](dcl.contract.func#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]")*s* ([[dcl.contract.func]](dcl.contract.func "9.4.1 General")), and[*assertion-statement*](stmt.contract.assert#nt:assertion-statement "8.9 Assertion statement [stmt.contract.assert]")*s* ([[stmt.contract.assert]](stmt.contract.assert "8.9 Assertion statement"))[.](#1.sentence-2)
|
||
|
||
[2](#2)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7578)
|
||
|
||
Each contract assertion has a [*contract-assertion predicate*](#def:predicate,contract-assertion "6.11.1 General [basic.contract.general]"),
|
||
which is an expression of type bool[.](#2.sentence-1)
|
||
|
||
[*Note [1](#note-1)*:
|
||
|
||
The value of the predicate is used to identify program states that are
|
||
expected[.](#2.sentence-2)
|
||
|
||
â *end note*]
|
||
|
||
[3](#3)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7587)
|
||
|
||
An invocation of the macro va_start ([[cstdarg.syn]](cstdarg.syn "17.14.2 Header <cstdarg> synopsis"))
|
||
shall not be a subexpression
|
||
of the predicate of a contract assertion,
|
||
no diagnostic required[.](#3.sentence-1)
|
||
|
||
[4](#4)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7593)
|
||
|
||
[*Note [2](#note-2)*:
|
||
|
||
Within the predicate of a contract assertion,[*id-expression*](expr.prim.id.general#nt:id-expression "7.5.5.1 General [expr.prim.id.general]")*s* referring to
|
||
variables declared outside the contract assertion
|
||
are const ([[expr.prim.id.unqual]](expr.prim.id.unqual "7.5.5.2 Unqualified names")),this is a pointer to const ([[expr.prim.this]](expr.prim.this "7.5.3 This")),
|
||
and the result object can be named
|
||
if a [*result-name-introducer*](dcl.contract.res#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") ([[dcl.contract.res]](dcl.contract.res "9.4.2 Referring to the result object")) has been specified[.](#4.sentence-1)
|
||
|
||
â *end note*]
|