Proving program correctness under all possible cases

Question

There are techniques of proving program correctness under all possible cases, but that is a more advanced topic, for a later subject in your curriculum.

I always had this doubt:

1. Is it possible to know all possible defects in a program before I write a single line of code? (i.e., How to detect a bug during the designing and planning stage itself.)

2. If yes, what are the strategies used by the professionals?

I've observed that if I am able to detect all possible logical flaws in designing and planning stage itself then overall development time is reduced. Currently to detect all possible flaws, I often run the program using all cases in my mind or on paper. As a senior engineer What techniques do you use?

Answer 1

Ensuring correctness of a computation mathematically is quite possible, just enormously expensive. Basically, you have to set down the requirements in a formal semantic system that is as rigid as a programming language itself. This involves an astonishing amount of work (contrary to popular opinion, requirements engineering is the hardest part of SE by far, much harder than coding).

You can do it if you have extremely important and slow-changing requirements and a client with very deep pockets - the standard example in the literature is the codebase of the systems that ran the Space Shuttle, which is considered the most correct large codebase in history. For almost all other projects, doing this is simply not cost-effective.

Answer 2

First you have to know what a "bug" is. In some projects this might be rigorously defined, in other projects it might be "I do not like the color". And opinions will differ about what is a bug or not, or what the "correct" behavior is, so this is much more complicated that it might first appear.

I would argue all projects are in some sense iterative. There will be cycles of planning, implementing and evaluation, so trying to find all issues before doing any implementation is doomed to failure. You should still try to find bugs and other problems as early as possible, but some issues will only be apparent when doing implementation. And you should be alert to "bugs" in all stages of development.

For user-facing applications, this might involve showing a prototype in front of a user, or user representative, as fast as possible. That should hopefully help with finding issues in the requirements.

Trying to predict problems often comes down to experience. The better you know the problem domain the less unexpected issues you will have, and the more the risk is reduced.

But once you have started writing a formal problem description (i.e. writing code) you can start using tools to help you. The first line of defense is usually the compiler, this will eliminate some classes of bugs. Then you have various types of analyzers that can help detect some types of bugs, but will have some false positives.

Then there is Automated testing. This can tell you if some specific input give correct output, but that require you to specify what the expected output is. This might range from unit testing where you test some small piece of code, to full scale simulations.

The sketching out all possible paths thru a program by hand is only possible for fairly small programs. It is a good approach to write "modules" that are small enough that this approach is applicable to the module in isolation.

But this still runs the risk leaky abstractions, where the abstractions you rely on does not quite match reality. As an example, you might treat a Double as 'real number', but this abstraction can fail, for example if you get a NaN as input. And when programs get large it becomes very difficult to predict how all modules will interact in all circumstances, even if you understand the "normal case" well enough. See Mars climate orbiter crash where different modules used different units, or Ariane 88 where a module where used outside of its original design parameters.

So my experience is that "proving correctness" by just analyzing code is of limited value. In practice you need testing, automated or not. The amount of testing is highly dependent on context, the testing regime for aviation software would be completely different from that of a game.

This is in principle not different from designing physical products. You should use the available tools to model behavior and help to predict failures. But you still need to test the thing to check that you have not missed something.

Answer 3

It seems noone here answered your literal question:

Is it possible to know all possible defects in a program before I write a single line of code

For this question, the answer is trivial: it is clearly no. When there is no code, you cannot even tell if your program has a syntactical error, since there is nothing to evaluate.

The answer by @KilianFoth has implicitly replaced the word "write" by "run" in your question (maybe because he assumed that's what you really wanted to know). If he got you right, follow his answer.

However, from what you wrote in the comments, I guess the question you really wanted to ask is

Is it possible to know all possible defects in a program's design before writing a single line of code

Here, the answer is still "no" - except for some very special scenarios. The reason is, typical software design artifacts, which are on a higher level of abstraction than code, are usually too informal to allow a rigorous proof of their defect-freeness. Typical design artifacts contain natural language, which cannot be rigidly tested like code. It is not even always obvious what a defect is. And even "design languages" like UML have often no strict semantics, which makes the line between correctness and incorrectness blurry.

Moreoever, when one puts also requirements under the umbrella of design and planning artifacts, it is should be clear you cannot decide if a requirement is "correct" or "incorrect", since requirements themselves are the benchmark for what is correct or incorrect.

However, that does not mean that all of this is in vain. Design artifacts and requirements can be analysed and reviewed by humans. Here systematic proofreading and walkthroughs by yourself or a second pairs of eyes is typically used for find inconsistencies or gaps in the design, or contradictions between requirements and design.

None of these techniques, however, can eliminate all potential issues, they can only lower the count. The ultimate test for a high-level design is when you start to implement parts of it in code, test that code and compare how well it maps to the requirements you want to achieve. That is why the most effective design validation technique is to implement parts in executable code, ideally in small iterative cycles, and not in a "Big-Design-Upfront".

Answer 4

While correctness of a program is generally very expensive to prove, there are a number of languages which strive (and fail) to isolate components achieving global correctness via provable local correctness.

The idea is to eliminate any language features that allow execution flow not lexically present in a scope of a single component.

• Joe-E
• Haskell
• Rust

Answer 5

The halting problem proof and Rices's theorem all prove that proving a program is correct is not decidable.

Why don't you look at the license agreements of anybody who sells software? As far as I can see, their lawyers all essentially say it is not guaranteed to be fit for a particular purpose, which basically says they don't claim it is correct.

Common Open Source:

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

Microsoft EULA:

12. DISCLAIMER OF WARRANTY.The software is licensed “as-is.” You bear the risk of using it. Microsoft gives no express warranties, guarantees or conditions. You may have additional consumer rights under your local laws which this agreement cannot change. To the extent permitted under your local laws, Microsoft excludes the implied warranties of merchantability, fitness for a particular purpose and non- infringement. FOR AUSTRALIA ONLY: You have statutory guarantees under the Australian Consumer Law and nothing in these terms is intended to affect those rights.

LIMITATION ON AND EXCLUSION OF REMEDIES AND DAMAGES. You can recover from Microsoft and its suppliers only direct damages up to U.S. $5.00. You can't recover any other damages, including consequential, lost profits, special, indirect or incidental damages.

Crowdstrike Terms and Conditions:

8.6 Disclaimer. EXCEPT FOR THE EXPRESS WARRANTIES IN THIS SECTION 8, CROWDSTRIKE AND ITS AFFILIATES DISCLAIM ALL OTHER WARRANTIES, WHETHER EXPRESS, IMPLIED, STATUTORY OR OTHERWISE. TO THE MAXIMUM EXTENT PERMITTED UNDER APPLICABLE LAW, CROWDSTRIKE AND ITS AFFILIATES AND SUPPLIERS SPECIFICALLY DISCLAIM ALL IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, TITLE, AND NON-INFRINGEMENT WITH RESPECT TO THE OFFERINGS AND CROWDSTRIKE TOOLS. THERE IS NO WARRANTY THAT THE OFFERINGS OR CROWDSTRIKE TOOLS WILL BE ERROR FREE, OR THAT THEY WILL OPERATE WITHOUT INTERRUPTION OR WILL FULFILL ANY OF CUSTOMER’S PARTICULAR PURPOSES OR NEEDS. THE OFFERINGS AND CROWDSTRIKE TOOLS ARE NOT FAULT-TOLERANT AND ARE NOT DESIGNED OR INTENDED FOR USE IN ANY HAZARDOUS ENVIRONMENT REQUIRING FAIL-SAFE PERFORMANCE OR OPERATION. NEITHER THE OFFERINGS NOR CROWDSTRIKE TOOLS ARE FOR USE IN THE OPERATION OF AIRCRAFT NAVIGATION, NUCLEAR FACILITIES, COMMUNICATION SYSTEMS, WEAPONS SYSTEMS, DIRECT OR INDIRECT LIFE-SUPPORT SYSTEMS, AIR TRAFFIC CONTROL, OR ANY APPLICATION OR INSTALLATION WHERE FAILURE COULD RESULT IN DEATH, SEVERE PHYSICAL INJURY, OR PROPERTY DAMAGE. Customer agrees that it is Customer’s responsibility to ensure safe use of an Offering and the CrowdStrike Tools in such applications and installations. CROWDSTRIKE DOES NOT WARRANT ANY THIRD PARTY PRODUCTS OR SERVICES.

Addendum: A Turing machine by Alan Turing's definition must halt to present a (presumably correct) solution. The proof Turing provided shows you can not prove it will ever halt. Rice's theorem is a more general proof of the same concept that also shows software cannot verify other software for correctness either. Wiki has excellent discussions on both you can refer to. These are actual mathematical proofs that as far as I know are not dis-proven by languages like Haskel, et al. Therefore programmer's who think they can actually prove 100% that nothing can go wrong are just fooling themselves. Those who mention hardware failures show some examples, but it doesn't even have to be a 'hard' failure, but also 'soft' failures caused by gamma radiation twiddling bits in memory. Fortunately, lawyers seem to be not as easily fooled, given the legal disclaimers they make sure are included with the product.

References:

https://en.wikipedia.org/wiki/Rice%27s_theorem

https://en.wikipedia.org/wiki/Halting_problem

https://en.wikipedia.org/wiki/Turing's_proof

https://en.wikipedia.org/wiki/Undecidable_problem