[SystemSafety] Number Theorist Fears All Published Math Is Wrong

Steve Tockey steve.tockey at construx.com
Tue Oct 29 20:42:42 CET 2019


Derek,

You wrote: “I am saying that proofs of correctness don't exist, only
evidence that certain kinds of behavior have not been found.”

That’s why I said that our respective definitions might be different.
Here’s what I mean:

1) It starts with the contract for an operation/method. What does it
require? The contract requires conditions (and any class invariants) can
be stated as propositions preceding the first line of executable method
code.

2) Between any pair of adjacent executable statements, there needs to be a
proposition that is consistent—in the propositional logic sense—with prior
propositions and the semantics of the programming language.


3) What does the contract guarantee? Contract guarantees conditions (and
class invariants) can be stated as propositions “following" each possible
exit (I say “following” because they are unreachable in an executability
sense).

As long as the intermediate proof propositions logically follow from
contract requires (and class invariants) to contract guarantees (and class
invariants) consistent with propositional logic and language semantics,
then it should demonstrate that the code does in fact satisfy the contract
(and class invariants).

Here is a real example for a Java operation/method that computes the
Internal Rate of Return (IRR) for a financial Cash Flow Stream (proof
propositions are shown as comments of the form “// { Px: proposition }”
where Px is a proposition identifier). Please excuse the periods in the
first column, Microsoft Outhouse (err, Outlook) on a Mac has a nasty
tendency to delete leading spaces which totally mucks up indentation.


- - - cut here - - -


.public class CashFlowStream {
.
.  // status value for returning an error on IRR calculations
.  public static final double IRR_ERROR = -999999.99;
.  // how close PW() at Estimated IRR needs to be to $0.00
.  private static final double MAX_DIFFERENCE = 0.01;
.
.  public double IRR() {
.  // requires
.  //   n/a
.  // guarantees
.  //   if IRR is meaningful for this cash flow stream
.  //      then its IRR is returned
.  //      otherwise CashFlowStream.IRR_ERROR is returned
.  // Implementation notes
.  //   uses the algorithm described on page 118 of Return on Software
.  //     any root solver could have been used, this was convenient
.    // { P0: Class invariants for CashFlowStream }
.    // initialize currentPW to PW( 0.0 )
.    double currentPW = this.PW( 0.0 );
.    // { P1: P0 and currentPW is double == PW( 0.0 ) of this CFS }
.    // Only calculate IRR if this cash flow stream is well-formed
.    if( this.firstNonZeroCashFlowIsNegative( ) &&
.        this.onlyOneSignChange( ) && this.PW( 0.0 ) > 0.00 ) {
.      // { P2: P1 and computing IRR is meaningful }
.      // start Estimated IRR at 0%
.      double estimatedIRR = 0.
.      // { P3: P2 and EstimatedIRR is double == 0. }
.      // start with Step Amount at +10%
.      double stepAmount = 10.
.      // { P4: P3 and stepAmount is double = 10. }
.      // iteratively narrow Estimated IRR until PW() close to $0.00
.      do {
.        // { P5 (Loop Invariant): P0 and
.        //        estimatedIRR is double >= 0. converging on actual IRR
and
.        //        abs( stepAmount ) is double <= 10. }
.        // refine Estimated IRR by one iteration
.          // save the previous PW at the old Estimated IRR
.          double lastPW = currentPW;
.          // { P6: P5 and lastPW is double == currentPW }
.          // move the Estimated IRR by the Step Amount
.          estimatedIRR = estimatedIRR + stepAmount;
.          // { P7: P6 and estimatedIRR has moved in
.          //              the direction & size of stepAmount }
.          // calculate the new PW at the new Estimated IRR
.          currentPW = this.PW( estimatedIRR );
.          // { P8: P7 and currentPW is double == PW at estimatedIRR }
.          // if new estimatedPW is farther from $0.00 than old
.          if( Math.abs( currentPW ) > Math.abs( lastPW ) ) {
.            // then cut Step Amount in half and switch direction
.            // { P9: P8 and estimatedIRR is farther from $0.00 }
.            stepAmount = -stepAmount / 2.0;
.            // { P10: P9 and stepAmount is reversed and halved }
.          }
.          // { P5 (Loop Invariant): P0 and
.          //        estimatedIRR is double >= 0. converging on actual IRR
and
.          //        abs( stepAmount ) is double <= 10. }
.        } while( Math.abs( currentPW ) > MAX_DIFFERENCE )
.        // { P11: P5 and currentPW is within MAX_DIFFERENCE of $0.00
.        //        (this is not B, the loop termination condition) }
.        // done narrowing, return Estimated IRR
.        return estimatedIRR;
.        // { P12: P0 and well formed CashFlowStream and
.        //               estimatedIRR was returned }
.      } else {
.        // { P13: P0 and not well formed CashFlowStream }
.        // not a well-formed CFS, return an error
.        return CashFlowStream.IRR_ERROR;
.        // { P14: P0 and not well formed CashFlowStream and
.        //               CashFlowStream.IRR_ERROR was returned }
.      }
.      // { P15: P0 and if this is a well formed CashFlowStream
.      //                 then IRR was returned
.      //                 else CashFlowStream.IRR_ERROR was returned }
.    }
.}


- - - cut here - - -

Doesn’t this prove that if:

*) the caller satisfied the requires clause (in this case, nothing), and

*) the class invariants were true going in (a necessary assumption)

Then, when the operation/method returns:

*) the class invariants are still true (but maybe temporarily false in the
middle), and
*) the contract guarantees conditions MUST be true


Per your statement, “. . . only evidence that certain kinds of behavior
have not been found”,

aren’t the "certain kinds of behavior" in this case exactly, "all
behaviors that are inconsistent with the class invariants and the
operation’s published contract”? If not, why not? And, if so, given that
all inconsistent behaviors have been proven to be impossible, doesn’t that
prove that only consistent (I.e., “correct”) behaviors are possible?

Did I not prove that the the method implementation satisfies the published
contract of the operation (and the class invariants)?


— steve




-----Original Message-----
From: Derek M Jones <derek at knosof.co.uk>
Organization: Knowledge Software, Ltd
Date: Tuesday, October 29, 2019 at 11:39 AM
To: Steve Tockey <Steve.Tockey at construx.com>,
"systemsafety at lists.techfak.uni-bielefeld.de"
<systemsafety at lists.techfak.uni-bielefeld.de>
Subject: Re: [SystemSafety] Number Theorist Fears All Published Math Is
Wrong

Steve,

> While I do not, unfortunately, have objective, independent, quantitative
> data to support the value of software proofs of correctness, I would like

I am saying that proofs of correctness don't exist, only evidence that
certain kinds of behavior have not been found.

As Martyn pointed out, some tools are capable of providing evidence
of certain characteristics under a very wide range of circumstances,
e.g., absence of any fixed-point overflow.

> to offer the following qualitative argument for why it should be taken a
> lot more seriously than it is.

My argument centers around cost benefit.

Show a worthwhile cost/benefit for a technique, and I'm sure lots of
people will take it more seriously.

>    Depending on testing alone to reveal software defects‹to demonstrate
> code correctness‹is a hopelessly lost cause

"code correctness" is a marketing term.

But in general, relying on any one technique can often be a lost cause.


-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com



More information about the systemsafety mailing list