You mention at the start of this post two sides of software correctness: doing what the programmer expects, and doing what the user needs. In engineering theory, these are usually respectively called verification and validation. All the examples given are verification methods.
For complex systems, verification and validation are related, in that a composite item will often be verified by relying on requirements that were passed to its components — and whether those requirements are correct is a validation question. Often, the validation problem is harder than verification, because it typically involves interfaces with other systems and with humans, and the expectations of those systems or humans may be ambiguous or even contradictory. Another important part of validation is expertise in adjacent fields, such as legal requirements for privacy, health, safety or environmental considerations.
Highly assured products will also often need verification methods beyond those described in this blog post. One manager of mine often said that for complex systems, it is impossible to test all the bugs out. He meant that both the specification and implementation of the system need to be done in a thoughtful, organized manner in order to provide confidence that defects have been systematically avoided or eliminated. Choosing airplanes and avionics as an example, simply reading the guidance documents — such as ARP4754A, ARP4761 and RTCA/DO-178C — will not readily give an understanding of the level of rigor that is required.
I use “assert” more and more in my code. It’s not exactly testing in the usual sense, but it helps me discover and repair coding errors quickly. It catches mistakes that I might otherwise never discover. It also serves as a kind of documentation, stating what my expectations are for a given block of code. I’ve never regretted adding more “asserts” in my code.
jldsays:
“It must meet the needs of the user.”
LMAO, in theory YES but what the user “want” (as far as they can articulate it 🙂 ) is NOT what the user need.
abstract_typesays:
Tests are entirely useless for correctness guarantees; at best, tests are a description of how some happy path works. Correctness is provided by construction (of a type) and composition (of smaller programs), and the easiest way to enable this is by a sound static type system which acts as a lightweight proof (as opposed to actual theorem provers like Coq, Agda etc).
Sushil Shresthasays:
“a sound static type system”… which lang is that ?
vladsays:
Some examples:
OCaml, F#, Scala (since version 3), Haskell, Rust.
anonsays:
They mentioned Coq and Agda. I’ll add Lean to that list of reasonable languages.
anonsays:
To quote a thesis which itself quotes ‘Dijkstra 1972. “Notes on structured programming”’.
> Testing can famously only prove the presence of bugs. [3]
> To prove that the language implementation satisfies the criteria on all inputs, one must turn to formal verification—i.e., by specifying it unambiguously in a formal language and giving a derivation that proves that it holds.
While this was the case in Dijkstra’s times, nowadays you often can test an algorithm on every possible input. This is called “brute force testing”. For example, you can test a math function on all float numbers. All of them.
Jamessays:
Excellent post, Daniel. You covered a lot of territory, and you covered it well.
I agree, excellent post, the coverage of the subject is good and down-to-earth.
A common saying we use at work is “If it is not tested, it does not work.”
I find it interesting that many programmers do not use basic accounting or tracking to manage their work. My company specializes in digital document conversion and finding errors would be a real nightmare if we didn’t have a method in place to track progress both forward and backward. This provides us a number of real benefits. Errors are VERY easy and quick to Identify, Processes are simple to audit back to failure and (I think best of all) you can repeat the entire process start to finish in the same manner the error was created to see if the changes in code were corrected.
Although I see many programmers create error reports, logs for install, debug and such I rarely see logs for processes work unless the end user wants them. It is very common in our company to create reports that link backwards and forwards to the processes and they are often stored in such a way they can be accessed and managed.
In the end George Carlin was right, you will never had a garage big enough to hold everything in the world you want and the same is true with logs and reports, but you can manage them. Even though they take up space and time they are valuable tracking and management tool.
While coding I am one of those people that does in line add debug processes etc. but in the end I find I remove them (or at least comment them out) until I create a version. I find that after the fact they are just clutter.
Very nice post. It’s a pity formal verification is not more advanced. Asserts, pre-conditions and post-conditions and TDD are really valuable to engage in a dialogue with your code that can make hidden assumptions explicit. Many bugs arise from implicit assumptions, IMHO.
You mention at the start of this post two sides of software correctness: doing what the programmer expects, and doing what the user needs. In engineering theory, these are usually respectively called verification and validation. All the examples given are verification methods.
For complex systems, verification and validation are related, in that a composite item will often be verified by relying on requirements that were passed to its components — and whether those requirements are correct is a validation question. Often, the validation problem is harder than verification, because it typically involves interfaces with other systems and with humans, and the expectations of those systems or humans may be ambiguous or even contradictory. Another important part of validation is expertise in adjacent fields, such as legal requirements for privacy, health, safety or environmental considerations.
Highly assured products will also often need verification methods beyond those described in this blog post. One manager of mine often said that for complex systems, it is impossible to test all the bugs out. He meant that both the specification and implementation of the system need to be done in a thoughtful, organized manner in order to provide confidence that defects have been systematically avoided or eliminated. Choosing airplanes and avionics as an example, simply reading the guidance documents — such as ARP4754A, ARP4761 and RTCA/DO-178C — will not readily give an understanding of the level of rigor that is required.
Thank you. You are correct.
I use “assert” more and more in my code. It’s not exactly testing in the usual sense, but it helps me discover and repair coding errors quickly. It catches mistakes that I might otherwise never discover. It also serves as a kind of documentation, stating what my expectations are for a given block of code. I’ve never regretted adding more “asserts” in my code.
“It must meet the needs of the user.”
LMAO, in theory YES but what the user “want” (as far as they can articulate it 🙂 ) is NOT what the user need.
Tests are entirely useless for correctness guarantees; at best, tests are a description of how some happy path works. Correctness is provided by construction (of a type) and composition (of smaller programs), and the easiest way to enable this is by a sound static type system which acts as a lightweight proof (as opposed to actual theorem provers like Coq, Agda etc).
“a sound static type system”… which lang is that ?
Some examples:
OCaml, F#, Scala (since version 3), Haskell, Rust.
They mentioned Coq and Agda. I’ll add Lean to that list of reasonable languages.
To quote a thesis which itself quotes ‘Dijkstra 1972. “Notes on structured programming”’.
> Testing can famously only prove the presence of bugs. [3]
> To prove that the language implementation satisfies the criteria on all inputs, one must turn to formal verification—i.e., by specifying it unambiguously in a formal language and giving a derivation that proves that it holds.
https://repository.tudelft.nl/islandora/object/uuid:f0312839-3444-41ee-9313-b07b21b59c11
While this was the case in Dijkstra’s times, nowadays you often can test an algorithm on every possible input. This is called “brute force testing”. For example, you can test a math function on all float numbers. All of them.
Excellent post, Daniel. You covered a lot of territory, and you covered it well.
Thank you.
I agree, excellent post, the coverage of the subject is good and down-to-earth.
A common saying we use at work is “If it is not tested, it does not work.”
I find it interesting that many programmers do not use basic accounting or tracking to manage their work. My company specializes in digital document conversion and finding errors would be a real nightmare if we didn’t have a method in place to track progress both forward and backward. This provides us a number of real benefits. Errors are VERY easy and quick to Identify, Processes are simple to audit back to failure and (I think best of all) you can repeat the entire process start to finish in the same manner the error was created to see if the changes in code were corrected.
Although I see many programmers create error reports, logs for install, debug and such I rarely see logs for processes work unless the end user wants them. It is very common in our company to create reports that link backwards and forwards to the processes and they are often stored in such a way they can be accessed and managed.
In the end George Carlin was right, you will never had a garage big enough to hold everything in the world you want and the same is true with logs and reports, but you can manage them. Even though they take up space and time they are valuable tracking and management tool.
While coding I am one of those people that does in line add debug processes etc. but in the end I find I remove them (or at least comment them out) until I create a version. I find that after the fact they are just clutter.
Just a typo:
(40000+4000)%65535=14464
should be
(40000+40000)%65536=14464
Very nice post. It’s a pity formal verification is not more advanced. Asserts, pre-conditions and post-conditions and TDD are really valuable to engage in a dialogue with your code that can make hidden assumptions explicit. Many bugs arise from implicit assumptions, IMHO.
It’s ‘quickly write’, not ‘write quickly’.
🙂