From 560668741bd3516347cc84dfa578ac0a19f5080d Mon Sep 17 00:00:00 2001 From: Andy Ko Date: Tue, 16 Apr 2019 14:37:47 -0700 Subject: [PATCH] Clarified automatic theorem provers. --- specifications.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specifications.html b/specifications.html index 61a4671..4894e71 100644 --- a/specifications.html +++ b/specifications.html @@ -70,11 +70,11 @@ function min(a, b) { } -

These two new lines of code are essentially functional specifications that declare "If either of those inputs is not an integer, the caller of this function is doing something wrong". This is useful to declare, but assertions have a bunch of problems: if your program can send a non-integer value to min, but you never test it in a way that does, you'll never see those alerts. This form of dynamic verification is therefore very limited, since it provides weaker guarantees about correctness. That said, a study of the use of assertions in a large database of GitHub projects shows that use of assertions is related to fewer defects (Casalnuovo et al. 2015) (though note that I said "related": we have no evidence that assertions actually prevent defects. It may be possible that developers who use assertions are just better at avoiding defects.)

+

These two new lines of code are essentially functional specifications that declare "If either of those inputs is not an integer, the caller of this function is doing something wrong". This is useful to declare, but assertions have a bunch of problems: if your program can send a non-integer value to min, but you never test it in a way that does, you'll never see those alerts. This form of dynamic verification is therefore very limited, since it provides weaker guarantees about correctness. That said, a study of the use of assertions in a large database of GitHub projects shows that use of assertions is related to fewer defects (Casalnuovo et al. 2015) (though note that I said "related": we have no evidence that assertions actually prevent defects. It may be possible that developers who use assertions are just better at avoiding defects.)

Assertions are related to the broader category of error handling language features. Error handling includes assertions, but also programming language features like exceptions and exception handlers. Error handling is a form of specification in that checking for errors usually entails explicitly specifying the conditions that determine an error. For example, in the code above, the condition Number.isInteger(a) specifies that the parameter a must be an integer. Other exception handling code such as the Java throws statement indicates the cases in which errors can occur and the corresponding catch statement indicates what is to done about errors. It is difficult to implement good exception handling that provides granular, clear ways of recovering from errors (Chen et al. 2009). Evidence shows that modern developers are still exceptionally bad at designing for errors; one study found that errors are not designed for, few errors are tested for, and exception handling is often overly general, providing little ability for users to understand errors or for developers to debug them (Ebert et al. 2015). These difficulties appear to be because it is difficult to imagine the vast range of errors that can occur (Maxion & Olszewski 2000).

-

Researchers have invented many forms of specification that require more work and more thought to write, but can be used to make stronger guarantees about correctness (Woodcock et al. 2009). For example, many languages support the expression of formal pre-conditions and post-conditions that represent contracts that must be kept. (Formal means mathematical, facilitating mathematical proofs that these conditions are met). Because these contracts are essentially mathematical promises, we can build tools that automatically read a function's code and verify that what it computes exhibits those mathematical properties using automated theorem proving systems. For example, suppose we wrote some formal specifications for our example above to replace our assertions (using a fictional notation for illustration purposes):

+

Researchers have invented many forms of specification that require more work and more thought to write, but can be used to make stronger guarantees about correctness (Woodcock et al. 2009). For example, many languages support the expression of formal pre-conditions and post-conditions that represent contracts that must be kept for the program to be corect. (Formal means mathematical, facilitating mathematical proofs that these conditions are met). Because these contracts are essentially mathematical promises, we can build tools that automatically read a function's code and verify that what it computes exhibits those mathematical properties using automated theorem proving systems. For example, suppose we wrote some formal specifications for our example above to replace our assertions (using a fictional notation for illustration purposes):

 // pre-conditions: a in Integers, b in Integers
@@ -84,7 +84,7 @@ function min(a, b) {
 }
-

The annotations above require that, no matter what, the inputs have to be integers and the output has to be less than or equal to both values. The automatic theorem prover can then start with the claim that result is always less than or equal to both and begin searching for a counterexample. Can you find a counterexample?

+

The annotations above require that, no matter what, the inputs have to be integers and the output has to be less than or equal to both values. The automatic theorem prover can then start with the claim that result is always less than or equal to both and begin searching for a counterexample. Can you find a counterexample? Really try. Think about what you're doing while you try: you're probably experimenting with different inputs to identify arguments that violate the contract. That's similar to what automatic theorem provers do, but they use many tricks to explore large possible spaces of inputs all at once, and they do it very quickly.

There are definite tradeoffs with writing detailed, formal specifications. The benefits are clear: many companies have written formal functional specifications in order to make completely unambiguous the required behavior of their code, particularly systems that are capable of killing people or losing money, such as flight automation software, banking systems, and even compilers that create executables from code (Woodcock et al. 2009). In these settings, it's worth the effort of being 100% certain that the program is correct because if it's not, people can die.