On Sat, 15 Oct 2016 10:44:06 -0400, Peter Relson wrote:
> 
>I believe COBOL V5 stated that recompile would work for correct programs. 
>I don't know if that statement is true or not, or what exactly is 
>definitively meant by "correct", but I think that ABO's more conservative 
>approach is expected to work even for programs that do not work upon 
>recompile with COBOL V5. Of course once one error has been found in an 
>implementation, most bets are off.
> 
When HLASM was introduced its documentation asserted that any
program that Assembler H assembled with no errors or warnings
would assemble identicallly with HLASM.  The refutation was trivial;
take any code with a construct undefined in H that HLASM assembled
differently.  That could even be leveraged into a Serious error in
HLASM.  IBM rapidly retracted the assertion.

I even have an ironic example where a program that HLASM assembles
differently with COMPAT(MACROCASE) but the same as H with
COMPAT(NOMACROCASE).

>... ignoring changes due to compile-date, ...
><snip>
>If by "certified" you basically mean "proved to be correct", how many 
>realistic programs are ever provably correct (many non-realistic programs 
>could be)? Surely a lot *are* correct, but could you prove it? I suspect 
>that most software companies "warrant" (if an error is reported, it may be 
>fixed) rather than "certify". 
> 
There are claims of general techniques for proving program correctness.
I disagree.  If the preprocessor is Turing-complete, correctness is
undecidable.  If one hedges by introducing a limit on program
complexity, that too may be undecidable even as Kolmogorov complexity
is uncomputable.

-- gil

----------------------------------------------------------------------
For IBM-MAIN subscribe / signoff / archive access instructions,
send email to lists...@listserv.ua.edu with the message: INFO IBM-MAIN

Reply via email to