[SystemSafety] Number Theorist Fears All Published Math Is Wrong

Steve Tockey steve.tockey at construx.com
Tue Oct 29 19:25:08 CET 2019


Derek, Martyn,
While I do not, unfortunately, have objective, independent, quantitative
data to support the value of software proofs of correctness, I would like
to offer the following qualitative argument for why it should be taken a
lot more seriously than it is.

By the way, this does assume that your definition of ³software proof of
correctness² is the same as mine. . .


- - - cut here - - -

Testing demonstrates proper behavior *only for the specific test cases
that were passed*. The following quote by Cem Kaner is appropriate:
 
 
  

  ³If you think you can fully test a program without testing its response
to every possible input, fine. Give us your test cases. We can write a
program that will pass all of your tests but still fail spectacularly on
an input you missed. If we can do this deliberately, our contention is
that we or other programmers could do it accidentally²

  
 
 
Code written without contracts and attention to simplicity & provability
would naturally be susceptible to semantic inconsistencies: defects.
Exhaustive testing of even simple code like the four-function calculator
in Chapter 12 is impossible. When scaled up to typical applications, it is
insane to think that testing could ever be anywhere close to comprehensive:

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

  
 
 
By proving code correct, there is less dependence on testing. Proven code
*cannot give anything other than the right answer*. Testing actually
becomes a way of validating the proof: if properly selected test cases
pass (e.g., test cases achieve decision coverage) then it is highly likely
that the proof is correct so you can be confident the code is correct for
all cases, not just the cases that were tested.


- - - end cut here - -


And,


- - - cut here - - -


Like Programming by intent, a Software proof of correctness is not
necessary or even appropriate for every method. Simple methods can be
straightforward enough that a proof may not add value. When a method is
non-trivial‹and particularly when defects could cause serious damage‹a
proof of correctness could be well worth the investment. We should even
question whether proofs are an extra investment. The effort needed to
prove code correct could easily be less than the effort needed to debug it
later, particularly if a defect is discovered months, or even years after
the code was last seen by developers. Why not develop software in a way
that minimizes the probability of defects in the first place:

 
*) The level of thinking needed to write correct code is the same level of
thinking needed to prove it correct
 
*) The level of thinking needed to fully determine the cause of some
failure, i.e., debugging, is the same level of thinking needed to prove it
correct
 
*) The level of thinking needed to fully verify a defect has been
eliminated is the same level of thinking needed to prove that code correct

Why not just use that level of thinking by proving the code correct from
the start? Time spent in up-front proof can be much less than time wasted
later debugging poorly written, incorrect code. Remember that Rework
Percentage, R%, is over 60% in typical software organizations. Proving
method code correct cannot take this much time.

 
Code doesn¹t always need to be *proven*, but it should always be
*provable*. Always write code to make proving it as easy as possible.
Consider the properties of a well-written mathematical proof:

 
*) Minimum number of steps
 
*) Clear, logical progression from one step to the next
 
*) Every step is necessary
 
*) All steps are sufficient

These same properties apply to well-written code. The process of creating
a good software proof leads to good code. Conversely, creating good code
makes it inherently provable.


- - - end cut here - - -


I would suggest that this qualitative reasoning should explain why it
would make sense to do an empirical study of the cost effectiveness of
software proof of correctness.

And, for what it¹s worth, there can be an interesting interplay between
proofs of correctness and use of assertions:


- - - cut here - - -

Kudrjavets et. al.[11] report a strong correlation between use of
assertions and a significant reduction in post-release defects. In two
different releases of two different code bases each having non-uniform
distribution of assertions, regions of code with more assertions had
statistically fewer post-release defects. As well, assertions revealed
defects that testing was unable to reveal. It is unlikely that the
presence of assertions alone caused this difference. A more likely
explanation is that proper use of assertions requires thinking about code
at a detailed semantic level. Developers who can use assertions properly
are probably more capable and are thus more likely to write correct code


[11] Gunnar Kudrjavets, Nachiappan Nagappan, Thomas Ball, ³The
relationship between software assertions and code quality², Embedded
Magazine, June 10, 2013. Available at:
http://research.microsoft.com/pubs/70290/tr-2006-54.pdf
 

- - - end cut here - -


Again, this is only qualitative data, but it suggests looking at how much
time was spent putting assertions into the code vs. how much time was
saved through earlier detection of defects. One might also be able to look
at defect density in code produced with and without assertions & proofs of
correctness. There¹s a non-zero chance that proper use of assertions &
proofs of correctness *avoids* defects. Defect avoidance needs to be
considered too, not just defect identification.



Regards,


‹ steve




-----Original Message-----
From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
on behalf of Derek M Jones <derek at knosof.co.uk>
Organization: Knowledge Software, Ltd
Date: Tuesday, October 29, 2019 at 10:41 AM
To: "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

Martyn,

> Your "open question" needs more constraints. How confident do you need
> to be that your software won't fail?

Exactly, what are the cost benefits.

> There are tools that can prove the absence of any fixed-point overflow
> in a program. for example, or show you exactly where it could occur. How
> long would it take you to do that by testing, in a program that
> calculates A, calculates B and then contains the expression 1/(A-B)   ?

There are tools that do particular tasks more cost effectively than
other tools.

> If you can't gain confidence about these small but important properties
> by testing the software, what exactly have you discovered by testing it
> and carefully checking the results - other than that it runs your test
> set correctly (in this particular order, today).

I am not proposing that writing test cases is the only technique
that should be used.

The more mathematical approaches can do some tasks more cost effectively
than writing test cases.

None of the available techniques proves correctness of the software.
They all operate by showing an absence of (presumably undesirable)
behavior.


> On 29/10/2019 16:27, Derek M Jones wrote:
>> David,
>>
>>> Have you every actually used a tool that attempts to provide formal
>>> proof of software correctness? If so, how many demonstrably false
>>
>> "formal proof of software correctness" is a meaningless marketing term.
>>
>> There are tools that show:
>>
>>     o for specified input, a specified list of expressions are true,
>>
>>     o that it was not possible to find any inconsistencies between
>> a specification and code claiming to implement the specification.
>>
>> These tools fail to find faults, just like testing.
>>
>> The open question is the extent to which they might, or might
>> not be more cost effective than testing.
>>
>>
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription:
>https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE
Manage your subscription:
https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety

-------------- next part --------------
A non-text attachment was scrubbed...
Name: default[2].xml
Type: application/xml
Size: 3222 bytes
Desc: default[2].xml
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191029/29247c66/attachment-0002.xml>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: default[3].xml
Type: application/xml
Size: 3222 bytes
Desc: default[3].xml
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191029/29247c66/attachment-0003.xml>


More information about the systemsafety mailing list