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 [email protected] with the message: INFO IBM-MAIN
