2710. "Effects: Equivalent to ..." doesn't count "Synchronization:" as determined semantics

Section: 16.3.2.4 [structure.specifications] Status: C++17 Submitter: Kazutoshi Satoda Opened: 2016-05-08 Last modified: 2017-07-30

Priority: 0

View other active issues in [structure.specifications].

View all other issues in [structure.specifications].

View all issues with C++17 status.

Discussion:

From N4582 17.5.1.4 [structure.specifications] p3 and p4

-3- Descriptions of function semantics contain the following elements (as appropriate):

• Requires: the preconditions for calling the function
• Effects: the actions performed by the function
• Synchronization: the synchronization operations (1.10) applicable to the function
• Postconditions: the observable results established by the function
• Returns: a description of the value(s) returned by the function
• Throws: any exceptions thrown by the function, and the conditions that would cause the exception
• Complexity: the time and/or space complexity of the function
• Remarks: additional semantic constraints on the function
• Error conditions: the error conditions for error codes reported by the function.
• Notes: non-normative comments about the function

-4- Whenever the Effects: element specifies that the semantics of some function F are Equivalent to some code sequence, then the various elements are interpreted as follows. If F's semantics specifies a Requires: element, then that requirement is logically imposed prior to the equivalent-to semantics. Next, the semantics of the code sequence are determined by the Requires:, Effects:, Postconditions:, Returns:, Throws:, Complexity:, Remarks:, Error conditions:, and Notes: specified for the function invocations contained in the code sequence. The value returned from F is specified by F's Returns: element, or if F has no Returns: element, a non-void return from F is specified by the Returns: elements in the code sequence. If F's semantics contains a Throws:, Postconditions:, or Complexity: element, then that supersedes any occurrences of that element in the code sequence.

The third sentence of p4 says "the semantics of the code sequence are determined by ..." and lists all elements in p3 except "Synchronization:".

I think it was just an oversight because p4 was added by library issue 997, and its proposed resolution was drafted at the time (2009) before "Synchronization:" was added into p3 for C++11.

However, I'm not definitely sure that it is really intended and safe to just supply "Synchronization:" in the list. (Could a library designer rely on this in writing new specifications, or could someone rely on this in writing user codes, after some years after C++11?)

Proposed resolution:

This wording is relative to N4582.

1. Change 16.3.2.4 [structure.specifications] as indicated:

   -4- Whenever the Effects: element specifies that the semantics of some function F are Equivalent to some code sequence, then the various elements are interpreted as follows. If F's semantics specifies a Requires: element, then that requirement is logically imposed prior to the equivalent-to semantics. Next, the semantics of the code sequence are determined by the Requires:, Effects:, Synchronization:, Postconditions:, Returns:, Throws:, Complexity:, Remarks:, Error conditions:, and Notes: specified for the function invocations contained in the code sequence. The value returned from F is specified by F's Returns: element, or if F has no Returns: element, a non-void return from F is specified by the Returns: elements in the code sequence. If F's semantics contains a Throws:, Postconditions:, or Complexity: element, then that supersedes any occurrences of that element in the code sequence.