Re: Compiler Correctness

The moderator nattered:

[Where I come from, with a given floating point arithmetic model,
there is only one correct result for each operation and one correct
representation for each input value. The ambiguities arise when a
compiler can use more than one possible sequence of operations to
evaluate an expression. -John]

Most languages allow the compiler some freedom in the evaluation of
expressions, including CSE and reordering of instructions and arguments.
What does this mean, with regards to the correctness of compilers for
such languages?

Ambiguities also can arise from different models or precision, as
implemented in specific FPU hardware. Doesn't this imply that a correct
compiler must emulate all floating point operations, so that the output
does not depend on the host machine of the compiler? The same for all
the target machines of an cross compiler...

The operation of the Intel coprocessor (x87) is configurable, and this
configuration can be changed at runtime. In this case a "correct"
compiler has to assure that, after every call to external code, the FPU
configuration is restored to the expected state.

At least these points should be considered in a proof of the correctness
of any program, including compilers.

DoDi
[You're right, some languages permit multiple floating point models. -John]
.

Relevant Pages

  • Re: methods with "short"-typed arguments.
    ... a programming language specification requires you to specify what ... I'd find it ok for the compiler to be fussy in light of two ... implicitly "upcasted" to int as needed, ... possible ambiguities of called methods the same way as with Classes, ...
    (comp.lang.java.programmer)
  • Re: Template file extension / inclusion / declaration
    ... > made available to the compiler: ... Because the linker cannot help us for template without the export ... there are some ambiguities to remove. ... >> decls by hand is really bad ...
    (comp.lang.cpp)
  • Re: delete
    ... >old compiler I have to figure out) but it's barely possible that the ... allowed the overloading of operator delete on void*&, ... ambiguities when you tried to use it: ... elaborated on why it's an exceedingly poor idea, but in your reply, you seem ...
    (microsoft.public.vc.language)
  • Re: delete
    ... > ambiguities when you tried to use it: ... compiler so defective as to allow it in the first place is likely to ... imagine the effects of moving to a newer one. ... use of this particular defect is a bad idea anyway. ...
    (microsoft.public.vc.language)
  • Re: Why C?
    ... > C programs can be as fast as a compiler can make them, ... > programs in other languages. ... > lurking bugs and inappropriate data types in any existing C code. ... With only a different declaration syntax it would be much ...
    (comp.os.linux.development.apps)