What is the definition of a "valid program"?

user_1778275 0
Viewed 184

ISO/IEC 9899:202x (E) working draft — December 11, 2020 N2596, footnote 9:

... an implementation is free to produce any number of diagnostic messages, often referred to as warnings, as long as a valid program is still correctly translated. It can also successfully translate an invalid program.

Searching the definition of "valid / invalid program" across the standard gives no results. In fact the footnote 9 is the only place where "valid / invalid program" is mentioned.

Note: yes:

In ISO standards, notes are without exception non-normative.

Source: https://www.iso.org/schema/isosts/v1.0/doc/n-6ew0.html.

However, people do frequently use the term "valid / invalid program".

Can someone please help to suggest / deduce the definition (relative to the standard) of the term "valid program"?

The question may look silly at the first glance. However, there are cases when people have different understandings of the term "valid program". Hence, misinterpretations occur.

My guess: valid program -- a program which does not violate any syntax rule or constraint.

Note: "semantics rule" is intentionally not included in this definition because per Rice's theorem "non-trivial semantic properties of programs are undecidable".

Is such definition appropriate? If no, then what it the appropriate definition?

c23 language-lawyer definition c
2 Answers

At least in older versions of the Standard, a Conforming C Program is any source text which is accepted by at least one Conforming C Implementation somewhere in the universe. Given that conforming implementations are allowed to extend the language to accept almost any arbitrary source text, including programs that contain constraint violations, provided that they only accept the latter after having issued at least one diagnostic, the question of whether any particular source text is a Conforming C Program is determined by the existence or non-existence of implementations that accept it, rather than by any trait of the source text itself.

user_3637510

Your assumption that a valid program may not violate any constraints is correct. And so is your assumption that correctness is impossible hard to prove via static analysis, but can only be attested to a specific execution pass.

It's the definition of the "invalid program" which is fuzzy. A program can still be valid for a limited set of inputs, so you can't label the program invalid entirely. Only programs which are invalid for every possible input are invalid as a whole. Likewise, only a program which is valid for every possible input is "truly valid". In reality, there is hardly any non-trivial program which would not have edge cases where it's still invalid.

To sum that up into a formal definition:

A program is valid if there is at least a single possible input for which no constraints are violated.

A program is invalid only if it violates constraints for all possible inputs.

And please don't confuse valid/invalid with correct/incorrect. Criteria for the later is correctness for all possible inputs.

user_28793250
Related