cplusplus / draft

C++ standards drafts
http://www.open-std.org/jtc1/sc22/wg21/
5.66k stars 748 forks source link

"Observable behavior" is not defined properly #3215

Open morinmorin opened 5 years ago

morinmorin commented 5 years ago

In [intro.abstract] p6, observable behavior is defined as

The least requirements on a conforming implementation are:

  • Accesses through volatile glvalues are evaluated strictly according to the rules of the abstract machine.
  • At program termination, all data written into files …
  • The input and output dynamics of interactive devices …

These collectively are referred to as the observable behavior of the program.

But, IIUC, "these" refer to the requirements and so this is not a proper definition of the observable behavior.

FrankHB commented 5 years ago

"Behavior" is not formally defined at all. ISO C has a definition. Add it to [defns] first?

morinmorin commented 5 years ago

PR (Possible Resolutions)

Simply enumerating what constitutes the observable behavior would be a clear resolution. Changing

These collectively are refered as the observable behavior …

to

The subjects of these requirements are collectively refered as the observable behavior …

might also work.

Related DR

The current wording was introduced in C++11 to resolve inconsistent execution requirements (and to consider threads):

C11 has similar wording:

The least requirements on a conforming implementation are: … This is the observable behavior of the program.

morinmorin commented 5 years ago

"Behavior" is not formally defined at all. ISO C has a definition.

Ah, it seems that C99 introduced the definition of behavior as "external appearance or action".

FrankHB commented 5 years ago

Ah, definition of behavior is related, but not the same problem here. It should better be fixed because not only observable behavior, but also other terms can rely it on, e.g. unspecific behavior and implementation-defined behavior.

But I think a normative definition of the term "behavior" is still helpful to resolve the problem.

Strictly speaking, the ISO C's definition of "behavior" can not be precisely covered by a formal model. Any expectation from users may have interactions (which seem out of the scope of this standard, but probably suitable in ISO/IEC 2382) with such a definition. What needed here is to make sure instances of "observable behavior" is a proper subset of those of "behavior" if we need the term behavior normatively. Same to unspecific behavior, and so on.

OTOH, observable behavior should allow a proper formalization to make the requirements clear, because the main purpose of the "observable" restriction over "behavior" is to make the expectation based on the abstract machine model (which should be ideally formalizable) explicit and precise. Hence, we can keep the existence of the differences about behavior between the abstract machine and conforming implementations in mind, even if we can't enumerate the precise instances of "behavior" in general. A normative definition of "behavior" can help readers to get the point.

Note ISO C also defines observable behavior, as:

The least requirements on a conforming implementation are: — Accesses to volatile objects are evaluated strictly according to the rules of the abstract machine. — At program termination, all data written into files shall be identical to the result that execution of the program according to the abstract semantics would have produced. — The input and output dynamics of interactive devices shall take place as specified in 7.21.3. The intent of these requirements is that unbuffered or line-buffered output appear as soon as possible, to ensure that prompting messages actually appear prior to a program waiting for input. This is the observable behavior of the program.

The wording uses "this" instead of "these requirements". This is grammatically more consistent with the definition of "behavior", though it also literally introduces the confusion: what is "this"? With the terminology of "behavior", it can be editorial, by interpreting "this" as the behavior of the program accepted by a conforming implementation.

However, there is another problem since CWG 785:

In [intro.abstract]/4:

A conforming implementation executing a well-formed program shall produce the same observable behavior as one of the possible executions of the corresponding instance of the abstract machine with the same program and the same input.

What is the "same" observable behavior, exactly?

Whether this problem is editorial or not, the suggested wording here should be compatible with the additional descriptions (if any).

jensmaurer commented 4 years ago

Editorial teleconference: CWG needs to review the rephrasing.