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

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

Priority: 0

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):

-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 20.4.1.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.