[dcl.attr.contract] Reorder paragraphs for more coherence.

Also move rules on virtual functions to [class.virtual].
Rephase assertion checking along pre/postcondition checking.

Author: jensmaurer

source/declarations.tex

@@ -4285,6 +4285,17 @@
 It expresses a condition that a function should ensure
 for the return value and/or the state of objects
 using a predicate that is intended to hold upon exit from the function.
+A postcondition may introduce an identifier to represent
+the glvalue result or the prvalue result object of the function.
+\begin{example}
+\begin{codeblock}
+int f(char * c)
+  [[ensures res: res > 0 && c != nullptr]];
+
+int g(double * p)
+  [[ensures audit res: res != 0 && p != nullptr && *p <= 0.0]];
+\end{codeblock}
+\end{example}
 
 \pnum
 A \grammarterm{contract-attribute-specifier} using \tcode{assert}
@@ -4333,15 +4344,30 @@
 and template parameters.
 
 \pnum
-An assertion is checked by evaluating its predicate.
-The predicate of an assertion is potentially evaluated\iref{basic.def.odr}.
-The predicate of an assertion is evaluated
-as part of the evaluation of the null statement\iref{stmt.expr} it applies to.
+\begin{note}
+A function pointer cannot include contract conditions.
+\begin{example}
+\begin{codeblock}
+typedef int (*fpt)() [[ensures r: r != 0]];     // error: contract condition not on a function declaration
+
+int g(int x) 
+  [[expects: x >= 0]] 
+  [[ensures r: r > x]]
+{
+  return x+1;
+}
+
+int (*pf)(int) = g;                             // OK
+int x = pf(5);                                  // contract conditions of \tcode{g} are checked
+\end{codeblock}
+\end{example}
+\end{note}
 
 \pnum
-The predicate of a contract condition
-is potentially evaluated\iref{basic.def.odr}
-and has the same semantic restrictions
+The predicate of a contract is potentially evaluated\iref{basic.def.odr}.
+
+\pnum
+The predicate of a contract condition has the same semantic restrictions
 as if it appeared as the first \grammarterm{expression-statement}
 in the body of the function it applies to.
 Additional access restrictions apply to names appearing in
@@ -4391,12 +4417,54 @@
 \end{codeblock}
 \end{example}
 
+\pnum
+A precondition is checked by evaluating its predicate
+immediately before starting evaluation of the function body.
+\begin{note}
+The function body includes
+the \grammarterm{function-try-block}\iref{except} and
+the \grammarterm{ctor-initializer}\iref{class.base.init}.
+\end{note}
+A postcondition is checked by evaluating its predicate
+immediately before returning control to the caller of the function.
+\begin{note}
+The lifetime of local variables and temporaries has ended.
+Exiting via an exception or via \tcode{longjmp}\iref{csetjmp.syn}
+is not considered returning control to the caller of the function.
+\end{note}
+
+\pnum
+If a function has multiple preconditions,
+their evaluation (if any) will be performed
+in the order they appear lexically.
+If a function has multiple postconditions,
+their evaluation (if any) will be performed
+in the order they appear lexically.
+\begin{example}
+\begin{codeblock}
+void f(int * p)
+  [[expects: p != nullptr]]                     // \#1
+  [[ensures: *p == 1]]                          // \#3
+  [[expects: *p == 0]]                          // \#2
+{
+  *p = 1;
+}
+\end{codeblock}
+\end{example}
+
+\pnum
+An assertion is checked by evaluating its predicate
+as part of the evaluation of the null statement\iref{stmt.expr}
+it applies to. 
+
 \pnum
 The only side effects of a predicate
 that are allowed in a \grammarterm{contract-attribute-specifier}
 are modifications of non-volatile objects
 whose lifetime began and ended within the evaluation of the predicate
 in functions invoked from that predicate.
+An evaluation of a predicate that exits via an exception
+invokes \tcode{std::terminate()}\iref{except.terminate}.
 The behavior of any other side effect is undefined.
 \begin{example}
 \begin{codeblock}
@@ -4424,6 +4492,34 @@
 \end{codeblock}
 \end{example}
 
+\pnum
+If a postcondition odr-uses\iref{basic.def.odr}
+a parameter value in its predicate
+and the function body makes direct or indirect modifications of that value,
+the behavior is undefined.
+\begin{example}
+\begin{codeblock}
+int f(int x)
+  [[ensures r: r == x]] 
+{
+  return ++x;                   // undefined behavior
+}
+
+int g(int * p)
+  [[ensures r: p != nullptr]] 
+{
+  *p = 42;                      // OK, \tcode{p} is not modified
+}
+
+int h(int x)
+  [[ensures r: r == x]]
+{
+  potentially_modify(x);        // undefined behavior if \tcode{x} is modified
+  return x;
+}
+\end{codeblock}
+\end{example}
+
 \pnum
 If the \grammarterm{contract-level}
 of a \grammarterm{contract-attribute-specifier} is absent,
@@ -4444,6 +4540,25 @@
 and are not evaluated at run-time.
 \end{note}
 
+\pnum
+Multiple contract conditions may be applied to a function type
+with the same or different \grammarterm{contract-level}{s}.
+\begin{example}
+\begin{codeblock}
+int z;
+
+bool is_prime(int k);
+
+void f(int x)
+  [[expects: x > 0]]
+  [[expects audit: is_prime(x)]]
+  [[ensures: z > 10]]
+{
+  @\commentellip@
+}
+\end{codeblock}
+\end{example}
+
 \pnum
 A translation may be performed
 with one of the following \defnx{build levels}{build level}:
@@ -4461,43 +4576,6 @@
 There should be no programmatic way of setting, modifying, or querying
 the build level of a translation unit.
 
-\pnum
-A precondition is checked by evaluating its predicate
-immediately before starting evaluation of the function body.
-\begin{note}
-The function body includes
-the \grammarterm{function-try-block}\iref{except} and
-the \grammarterm{ctor-initializer}\iref{class.base.init}.
-\end{note}
-A postcondition is checked by evaluating its predicate
-immediately before returning control to the caller of the function.
-\begin{note}
-The lifetime of local variables and temporaries has ended.
-Exiting via an exception or via \tcode{longjmp}\iref{csetjmp.syn}
-is not considered returning control to the caller of the function.
-\end{note}
-An evaluation of a predicate that exits via an exception
-invokes \tcode{std::terminate()}\iref{except.terminate}.
-
-\pnum
-If a function has multiple preconditions,
-their evaluation (if any) will be performed
-in the order they appear lexically.
-If a function has multiple postconditions,
-their evaluation (if any) will be performed
-in the order they appear lexically.
-\begin{example}
-\begin{codeblock}
-void f(int * p)
-  [[expects: p != nullptr]]                     // \#1
-  [[ensures: *p == 1]]                          // \#3
-  [[expects: *p == 0]]                          // \#2
-{
-  *p = 1;
-}
-\end{codeblock}
-\end{example}
-
 \pnum
 It is unspecified whether a contract
 that would not be checked under the current build level is evaluated.
@@ -4577,125 +4655,4 @@
 \end{codeblock}
 \end{example}
 
-\rSec3[dcl.attr.contract.iface]{Interface contracts}%
-
-\pnum
-Multiple contract conditions may be applied to a function type
-with the same or different \grammarterm{contract-level}{s}.
-\begin{example}
-\begin{codeblock}
-int z;
-
-bool is_prime(int k);
-
-void f(int x)
-  [[expects: x > 0]]
-  [[expects audit: is_prime(x)]]
-  [[ensures: z > 10]]
-{
-  @\commentellip@
-}
-\end{codeblock}
-\end{example}
-
-\pnum
-A postcondition may introduce an identifier to represent
-the glvalue result or the prvalue result object of the function.
-\begin{example}
-\begin{codeblock}
-int f(char * c)
-  [[ensures res: res > 0 && c != nullptr]];
-
-int g(double * p)
-  [[ensures audit res: res != 0 && p != nullptr && *p <= 0.0]];
-\end{codeblock}
-\end{example}
-
-\pnum
-If a postcondition odr-uses\iref{basic.def.odr}
-a parameter value in its predicate
-and the function body makes direct or indirect modifications of that value,
-the behavior is undefined.
-\begin{example}
-\begin{codeblock}
-int f(int x)
-  [[ensures r: r == x]]
-{
-  return ++x;                   // undefined behavior
-}
-
-int g(int * p)
-  [[ensures r: p != nullptr]]
-{
-  *p = 42;                      // OK, \tcode{p} is not modified
-}
-
-int h(int x)
-  [[ensures r: r == x]]
-{
-  potentially_modify(x);        // undefined behavior if \tcode{x} is modified
-  return x;
-}
-\end{codeblock}
-\end{example}
-
-\pnum
-\begin{note}
-A function pointer cannot include contract conditions.
-\begin{example}
-\begin{codeblock}
-typedef int (*fpt)() [[ensures r: r != 0]];     // error: contract condition not on a function declaration
-
-int g(int x)
-  [[expects: x >= 0]]
-  [[ensures r: r > x]]
-{
-  return x+1;
-}
-
-int (*pf)(int) = g;                             // OK
-int x = pf(5);                                  // contract conditions of \tcode{g} are checked
-\end{codeblock}
-\end{example}
-\end{note}
-
-\pnum
-If an overriding function specifies contract conditions,
-it shall specify the same list of contract conditions as
-its overridden functions;
-no diagnostic is required
-if corresponding conditions will always evaluate to the same value.
-Otherwise, it is considered to have
-the list of contract conditions from one of its overridden functions;
-the names in the contract conditions are bound,
-and the semantic constraints are checked,
-at the point where the contract conditions appear.
-Given a virtual function \tcode{f}
-with a contract condition that odr-uses \tcode{*this}\iref{basic.def.odr},
-the class of which \tcode{f} is a direct member
-shall be be an unambiguous and accessible base class of any class
-in which \tcode{f} is overridden.
-If a function overrides more than one function,
-all of the overridden functions shall have
-the same list of contract conditions\iref{dcl.attr.contract};
-no diagnostic is required
-if corresponding conditions will always evaluate to the same value.
-\begin{example}
-\begin{codeblock}
-struct A {
-  virtual void g() [[expects: x == 0]];
-  int x = 42;
-};
-
-int x = 42;
-struct B {
-  virtual void g() [[expects: x == 0]];
-}
-
-struct C : A, B {
-  virtual void g();             // ill-formed, no diagnostic required
-};
-\end{codeblock}
-\end{example}
-
 \indextext{attribute!contracts|)}

source/derived.tex

@@ -911,9 +911,43 @@
 \indextext{function!virtual|)}
 
 \pnum
-\begin{note}
-For contracts, see \ref{dcl.attr.contract.iface}.
-\end{note}
+If an overriding function specifies contract conditions\iref{dcl.attr.contract},
+it shall specify the same list of contract conditions as
+its overridden functions;
+no diagnostic is required
+if corresponding conditions will always evaluate to the same value.
+Otherwise, it is considered to have
+the list of contract conditions from one of its overridden functions;
+the names in the contract conditions are bound,
+and the semantic constraints are checked,
+at the point where the contract conditions appear.
+Given a virtual function \tcode{f}
+with a contract condition that odr-uses \tcode{*this}\iref{basic.def.odr},
+the class of which \tcode{f} is a direct member
+shall be be an unambiguous and accessible base class of any class
+in which \tcode{f} is overridden.
+If a function overrides more than one function,
+all of the overridden functions shall have
+the same list of contract conditions\iref{dcl.attr.contract};
+no diagnostic is required
+if corresponding conditions will always evaluate to the same value.
+\begin{example}
+\begin{codeblock}
+struct A {
+  virtual void g() [[expects: x == 0]];
+  int x = 42;
+};
+
+int x = 42;
+struct B {
+  virtual void g() [[expects: x == 0]];
+}
+
+struct C : A, B {
+  virtual void g();             // ill-formed, no diagnostic required
+};
+\end{codeblock}
+\end{example}
 
 \rSec1[class.abstract]{Abstract classes}%