495 lines
19 KiB
Markdown
495 lines
19 KiB
Markdown
[basic.contract]
|
||
|
||
# 6 Basics [[basic]](./#basic)
|
||
|
||
## 6.11 Contract assertions [basic.contract]
|
||
|
||
### [6.11.1](#general) General [[basic.contract.general]](basic.contract.general)
|
||
|
||
[1](#general-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[.](#general-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"))[.](#general-1.sentence-2)
|
||
|
||
[2](#general-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[.](#general-2.sentence-1)
|
||
|
||
[*Note [1](#general-note-1)*:
|
||
|
||
The value of the predicate is used to identify program states that are
|
||
expected[.](#general-2.sentence-2)
|
||
|
||
â *end note*]
|
||
|
||
[3](#general-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[.](#general-3.sentence-1)
|
||
|
||
[4](#general-4)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7593)
|
||
|
||
[*Note [2](#general-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[.](#general-4.sentence-1)
|
||
|
||
â *end note*]
|
||
|
||
### [6.11.2](#eval) Evaluation [[basic.contract.eval]](basic.contract.eval)
|
||
|
||
[1](#eval-1)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7606)
|
||
|
||
An evaluation of a contract assertion
|
||
uses one of the following four [*evaluation semantics*](#def:evaluation_semantics "6.11.2 Evaluation [basic.contract.eval]"):[*ignore*](#def:contract_evaluation_semantics,ignore "6.11.2 Evaluation [basic.contract.eval]"),[*observe*](#def:contract_evaluation_semantics,observe "6.11.2 Evaluation [basic.contract.eval]"),[*enforce*](#def:contract_evaluation_semantics,enforce "6.11.2 Evaluation [basic.contract.eval]"), or[*quick-enforce*](#def:contract_evaluation_semantics,quick-enforce "6.11.2 Evaluation [basic.contract.eval]")[.](#eval-1.sentence-1)
|
||
|
||
Observe, enforce, and quick-enforce are [*checking semantics*](#def:contract_evaluation_semantics,checking "6.11.2 Evaluation [basic.contract.eval]");
|
||
enforce and quick-enforce are [*terminating semantics*](#def:contract_evaluation_semantics,terminating "6.11.2 Evaluation [basic.contract.eval]")[.](#eval-1.sentence-2)
|
||
|
||
[2](#eval-2)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7619)
|
||
|
||
It isimplementation-defined
|
||
which evaluation semantic is used
|
||
for any given evaluation of a contract assertion[.](#eval-2.sentence-1)
|
||
|
||
[*Note [1](#eval-note-1)*:
|
||
|
||
The range and flexibility of available choices of
|
||
evaluation semantics depends on the implementation
|
||
and need not allow all four evaluation semantics as possibilities[.](#eval-2.sentence-2)
|
||
|
||
The evaluation semantics can differ
|
||
for different evaluations of the same contract assertion,
|
||
including evaluations during constant evaluation[.](#eval-2.sentence-3)
|
||
|
||
â *end note*]
|
||
|
||
[3](#eval-3)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7633)
|
||
|
||
*Recommended practice*: An implementation should provide
|
||
the option to translate a program
|
||
such that all evaluations of contract assertions use the ignore semantic
|
||
as well as
|
||
the option to translate a program
|
||
such that all evaluations of contract assertions use the enforce semantic[.](#eval-3.sentence-1)
|
||
|
||
By default,
|
||
evaluations of contract assertions should use the enforce semantic[.](#eval-3.sentence-2)
|
||
|
||
[4](#eval-4)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7644)
|
||
|
||
The evaluation of a contract assertion using the ignore semantic has no effect[.](#eval-4.sentence-1)
|
||
|
||
[*Note [2](#eval-note-2)*:
|
||
|
||
The predicate is potentially evaluated ([[basic.def.odr]](basic.def.odr "6.3 One-definition rule")),
|
||
but not evaluated[.](#eval-4.sentence-2)
|
||
|
||
â *end note*]
|
||
|
||
[5](#eval-5)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7651)
|
||
|
||
The evaluation A of a contract assertion
|
||
using a checking semantic
|
||
determines the value of the predicate[.](#eval-5.sentence-1)
|
||
|
||
It is unspecified
|
||
whether the predicate is evaluated[.](#eval-5.sentence-2)
|
||
|
||
Let B be the value that would result from evaluating the predicate[.](#eval-5.sentence-3)
|
||
|
||
[*Note [3](#eval-note-3)*:
|
||
|
||
To determine whether a predicate would evaluate
|
||
to true or false,
|
||
an alternative evaluation
|
||
that produces the same value as the predicate
|
||
but has no side effects
|
||
can occur[.](#eval-5.sentence-4)
|
||
|
||
[*Example [1](#eval-example-1)*: struct S {mutable int g = 5;} s;void f() pre(( s.g++, false )); // #1void g(){ f(); // Increment of s.g might not occur, even if #1 uses a checking semantic.} â *end example*]
|
||
|
||
â *end note*]
|
||
|
||
[6](#eval-6)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7680)
|
||
|
||
There is an observable checkpoint ([[intro.abstract]](intro.abstract "4.1.2 Abstract machine")) C that happens before A such that any other operation O that happens before A also happens before C[.](#eval-6.sentence-1)
|
||
|
||
[7](#eval-7)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7687)
|
||
|
||
A [*contract violation*](#def:contract_violation "6.11.2 Evaluation [basic.contract.eval]") occurs when
|
||
|
||
- [(7.1)](#eval-7.1)
|
||
|
||
B is false,
|
||
|
||
- [(7.2)](#eval-7.2)
|
||
|
||
the evaluation of the predicate
|
||
exits via an exception, or
|
||
|
||
- [(7.3)](#eval-7.3)
|
||
|
||
the evaluation of the predicate
|
||
is performed in a context that is
|
||
manifestly constant-evaluated ([[expr.const]](expr.const "7.7 Constant expressions"))
|
||
and the predicate
|
||
is not a core constant expression[.](#eval-7.sentence-1)
|
||
|
||
[*Note [4](#eval-note-4)*:
|
||
|
||
If B is true,
|
||
no contract violation occurs and
|
||
control flow continues normally
|
||
after the point of evaluation of the contract assertion[.](#eval-7.sentence-2)
|
||
|
||
The evaluation of the predicate
|
||
can fail to produce a value
|
||
without causing a contract violation,
|
||
for example,
|
||
by calling longjmp ([[csetjmp.syn]](csetjmp.syn "17.14.3 Header <csetjmp> synopsis"))
|
||
or terminating the program[.](#eval-7.sentence-3)
|
||
|
||
â *end note*]
|
||
|
||
[8](#eval-8)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7716)
|
||
|
||
If a contract violation occurs
|
||
in a context that is manifestly constant-evaluated ([[expr.const]](expr.const "7.7 Constant expressions")),
|
||
and the evaluation semantic is
|
||
a terminating semantic,
|
||
the program is ill-formed[.](#eval-8.sentence-1)
|
||
|
||
[*Note [5](#eval-note-5)*:
|
||
|
||
A diagnostic is produced
|
||
if the evaluation semantic is observe ([[intro.compliance]](intro.compliance "4.1 Implementation compliance"))[.](#eval-8.sentence-2)
|
||
|
||
â *end note*]
|
||
|
||
[*Note [6](#eval-note-6)*:
|
||
|
||
Different evaluation semantics
|
||
chosen for the same contract assertion
|
||
in different translation units
|
||
can result in
|
||
violations of the one-definition rule ([[basic.def.odr]](basic.def.odr "6.3 One-definition rule"))
|
||
when a contract assertion has side effects
|
||
that alter the value produced by a constant expression[.](#eval-8.sentence-3)
|
||
|
||
[*Example [2](#eval-example-2)*: constexpr int f(int i){contract_assert((++const_cast<int&>(i), true)); return i;}inline void g(){int a[f(1)]; // size dependent on the evaluation semantic of contract_assert above} â *end example*]
|
||
|
||
â *end note*]
|
||
|
||
[9](#eval-9)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7752)
|
||
|
||
When the program is [*contract-terminated*](#def:contract-terminated "6.11.2 Evaluation [basic.contract.eval]"),
|
||
it isimplementation-defined
|
||
(depending on context) whether
|
||
|
||
- [(9.1)](#eval-9.1)
|
||
|
||
std::terminate is called,
|
||
|
||
- [(9.2)](#eval-9.2)
|
||
|
||
std::abort is called, or
|
||
|
||
- [(9.3)](#eval-9.3)
|
||
|
||
execution is terminated[.](#eval-9.sentence-1)
|
||
[*Note [7](#eval-note-7)*:
|
||
No further execution steps occur ([[intro.progress]](intro.progress "6.10.2.3 Forward progress"))[.](#eval-9.3.sentence-2)
|
||
â *end note*]
|
||
|
||
[*Note [8](#eval-note-8)*:
|
||
|
||
Performing the actions ofstd::terminate or std::abort without actually making a library call
|
||
is a conforming implementation of
|
||
contract-termination ([[intro.abstract]](intro.abstract "4.1.2 Abstract machine"))[.](#eval-9.sentence-2)
|
||
|
||
â *end note*]
|
||
|
||
[10](#eval-10)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7778)
|
||
|
||
If a contract violation occurs
|
||
in a context that is not manifestly constant-evaluated
|
||
and the evaluation semantic is quick-enforce,
|
||
the program is contract-terminated[.](#eval-10.sentence-1)
|
||
|
||
[11](#eval-11)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7786)
|
||
|
||
If a contract violation occurs
|
||
in a context that is not manifestly constant-evaluated
|
||
and the evaluation semantic is enforce or observe,
|
||
the contract-violation handler ([[basic.contract.handler]](#handler "6.11.3 Contract-violation handler"))
|
||
is invoked with an lvalue referring to
|
||
an object v of type const std::contracts::contract_violation ([[support.contract.violation]](support.contract.violation "17.10.3 Class contract_violation"))
|
||
containing information about the contract violation[.](#eval-11.sentence-1)
|
||
|
||
Storage for v is allocated in an unspecified manner
|
||
except as noted in [[basic.stc.dynamic.allocation]](basic.stc.dynamic.allocation "6.8.6.5.2 Allocation functions")[.](#eval-11.sentence-2)
|
||
|
||
The lifetime of v persists for the duration
|
||
of the invocation of the contract-violation handler[.](#eval-11.sentence-3)
|
||
|
||
[12](#eval-12)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7806)
|
||
|
||
If the contract violation occurred
|
||
because the evaluation of the predicate
|
||
exited via an exception,
|
||
the contract-violation handler is invoked
|
||
from within an active implicit handler
|
||
for that exception ([[except.handle]](except.handle "14.4 Handling an exception"))[.](#eval-12.sentence-1)
|
||
|
||
If the contract-violation handler
|
||
returns normally
|
||
and the evaluation semantic is observe,
|
||
that implicit handler
|
||
is no longer considered active[.](#eval-12.sentence-2)
|
||
|
||
[*Note [9](#eval-note-9)*:
|
||
|
||
The exception can be inspected or rethrown within the contract-violation handler[.](#eval-12.sentence-3)
|
||
|
||
â *end note*]
|
||
|
||
[13](#eval-13)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7823)
|
||
|
||
If the contract-violation handler
|
||
returns normally
|
||
and the evaluation semantic is enforce,
|
||
the program is contract-terminated;
|
||
if violation occurred
|
||
as the result of an uncaught exception
|
||
from the evaluation of the predicate,
|
||
the implicit handler
|
||
remains active when contract termination occurs[.](#eval-13.sentence-1)
|
||
|
||
[14](#eval-14)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7835)
|
||
|
||
[*Note [10](#eval-note-10)*:
|
||
|
||
If the contract-violation handler
|
||
returns normally
|
||
and the evaluation semantic is observe,
|
||
control flow continues normally
|
||
after the point of evaluation of the contract assertion[.](#eval-14.sentence-1)
|
||
|
||
â *end note*]
|
||
|
||
[15](#eval-15)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7845)
|
||
|
||
There is an observable checkpoint ([[intro.abstract]](intro.abstract "4.1.2 Abstract machine")) C that happens after the contract-violation handler returns normally
|
||
such that any other operation O that happens after the contract-violation handler returns
|
||
also happens after C[.](#eval-15.sentence-1)
|
||
|
||
[16](#eval-16)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7852)
|
||
|
||
[*Note [11](#eval-note-11)*:
|
||
|
||
The terminating semantics terminate the program
|
||
if execution would otherwise continue normally
|
||
past a contract violation:
|
||
the enforce semantic provides the opportunity to
|
||
log information about the contract violation
|
||
before terminating the program
|
||
or to throw an exception to avoid termination,
|
||
and the quick-enforce semantic is intended
|
||
to terminate the program as soon as possible
|
||
as well as
|
||
to minimize the impact of contract checks
|
||
on the generated code size[.](#eval-16.sentence-1)
|
||
|
||
Conversely,
|
||
the observe semantic
|
||
provides the opportunity to
|
||
log information about the contract violation
|
||
without having to terminate the program[.](#eval-16.sentence-2)
|
||
|
||
â *end note*]
|
||
|
||
[17](#eval-17)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7873)
|
||
|
||
If a contract-violation handler
|
||
invoked from the evaluation of a function contract assertion ([[dcl.contract.func]](dcl.contract.func "9.4.1 General"))
|
||
exits via an exception,
|
||
the behavior is as if
|
||
the function body exits via that same exception[.](#eval-17.sentence-1)
|
||
|
||
[*Note [12](#eval-note-12)*:
|
||
|
||
A [*function-try-block*](except.pre#nt:function-try-block "14.1 Preamble [except.pre]") ([[except.pre]](except.pre "14.1 Preamble"))
|
||
is the function body when present
|
||
and thus does not
|
||
have an opportunity to catch the exception[.](#eval-17.sentence-2)
|
||
|
||
If the function
|
||
has a non-throwing exception specification,
|
||
the function std::terminate is invoked ([[except.terminate]](except.terminate "14.6.2 The std::terminate function"))[.](#eval-17.sentence-3)
|
||
|
||
â *end note*]
|
||
|
||
[*Note [13](#eval-note-13)*:
|
||
|
||
If a contract-violation handler
|
||
invoked from an [*assertion-statement*](stmt.contract.assert#nt:assertion-statement "8.9 Assertion statement [stmt.contract.assert]") ([[stmt.contract.assert]](stmt.contract.assert "8.9 Assertion statement"))
|
||
exits via an exception,
|
||
the search for a handler
|
||
continues from the execution of that statement[.](#eval-17.sentence-4)
|
||
|
||
â *end note*]
|
||
|
||
[18](#eval-18)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7897)
|
||
|
||
To [*evaluate in sequence*](#def:evaluate_in_sequence "6.11.2 Evaluation [basic.contract.eval]") a list R of contract assertions:
|
||
|
||
- [(18.1)](#eval-18.1)
|
||
|
||
Construct a list of contract assertions S such that
|
||
* [(18.1.1)](#eval-18.1.1)
|
||
|
||
all elements of R are in S,
|
||
|
||
* [(18.1.2)](#eval-18.1.2)
|
||
|
||
each element of R may be repeated animplementation-defined
|
||
number of times
|
||
within S, and
|
||
|
||
* [(18.1.3)](#eval-18.1.3)
|
||
|
||
if a contract assertion A precedes another contract assertion B in R,
|
||
then the
|
||
first occurrence of A precedes the first occurrence of B in S[.](#eval-18.1.sentence-1)
|
||
|
||
- [(18.2)](#eval-18.2)
|
||
|
||
Evaluate each element of S such that,
|
||
if a contract assertion A precedes a contract assertion B in S,
|
||
then the evaluation of A is sequenced before
|
||
the evaluation of B[.](#eval-18.2.sentence-1)
|
||
|
||
[*Example [3](#eval-example-3)*: void f(int i){contract_assert(i > 0); // #1contract_assert(i < 10); // #2// valid sequence of evaluations: #1 #2// valid sequence of evaluations: #1 #1 #2 #2// valid sequence of evaluations: #1 #2 #1 #2// valid sequence of evaluations: #1 #2 #2 #1// invalid sequence of evaluations: #2 #1} â *end example*]
|
||
|
||
[19](#eval-19)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7945)
|
||
|
||
*Recommended practice*: An implementation should
|
||
provide an option to perform
|
||
a specified number of repeated evaluations
|
||
for contract assertions[.](#eval-19.sentence-1)
|
||
|
||
By default,
|
||
no repeated evaluations should be performed[.](#eval-19.sentence-2)
|
||
|
||
### [6.11.3](#handler) Contract-violation handler [[basic.contract.handler]](basic.contract.handler)
|
||
|
||
[1](#handler-1)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7956)
|
||
|
||
The [*contract-violation handler*](#def:contract-violation_handler "6.11.3 Contract-violation handler [basic.contract.handler]") of a program is a function named::handle_contract_violation[.](#handler-1.sentence-1)
|
||
|
||
The contract-violation handler
|
||
shall have a single parameter
|
||
of type
|
||
âlvalue reference to const std::contracts::contract_violationâ
|
||
and shall return void[.](#handler-1.sentence-2)
|
||
|
||
The contract-violation handler
|
||
may have a non-throwing exception specification[.](#handler-1.sentence-3)
|
||
|
||
The implementation
|
||
shall provide a definition of the contract-violation handler,
|
||
called the [*default contract-violation handler*](#def:contract-violation_handler,default "6.11.3 Contract-violation handler [basic.contract.handler]")[.](#handler-1.sentence-4)
|
||
|
||
[*Note [1](#handler-note-1)*:
|
||
|
||
No declaration
|
||
for the default contract-violation handler
|
||
is provided by
|
||
any standard library header[.](#handler-1.sentence-5)
|
||
|
||
â *end note*]
|
||
|
||
[2](#handler-2)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7979)
|
||
|
||
*Recommended practice*: The default contract-violation handler
|
||
should produce diagnostic output
|
||
that suitably formats the most relevant contents
|
||
of the std::contracts::contract_violation object,
|
||
rate-limited for potentially repeated violations
|
||
of observed contract assertions,
|
||
and then return normally[.](#handler-2.sentence-1)
|
||
|
||
[3](#handler-3)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/basic.tex#L7989)
|
||
|
||
It isimplementation-defined
|
||
whether the contract-violation handler
|
||
is replaceable ([[dcl.fct.def.replace]](dcl.fct.def.replace#term.replaceable.function "9.6.5 Replaceable function definitions"))[.](#handler-3.sentence-1)
|
||
|
||
If the contract-violation handler
|
||
is not replaceable,
|
||
a declaration of a replacement function for the contract-violation handler
|
||
is ill-formed, no diagnostic required[.](#handler-3.sentence-2)
|