In order to better understand proofs, I am wondering if the following example will help clarify. Given the following JavaScript function:

function log(a) {
  console.log(a)
}

My questions are:

  1. If it is possible to create a specification around this, and prove "correctness" to the specification.
  2. All the ways we can write tests for this to verify that "it works as expected" (writing proofs, abstract interpretation, model checking, unit tests, etc.).

If this were a unit test, it could be along the lines of:

// in node.js I would use the process.stdout, but this is for demo purposes:
var calls = []
var old = console.log
console.log = function(a){ calls.push(a) }
log('hello world')
console.log = old
assert(calls[0] == 'hello world')

Essentially with TDD, you just test the method gets called with some parameters. But then the question is, what about proving it will log the output. Wondering if it's possible to write a "proof" somehow, or if proofs do not apply (wondering why not in that case).

My program proves console.log will print its parameter.

Model checking can be used to try arbitrary combinations of input and see that it prints the output, so that makes sense. I'm really wondering about the concept of proofs in situations like these (proving arbitrary code snippets do what you want them to). Say you had something slightly more complex like an HTTP request, and that you will handle the error, or drawing to the screen, that it is a certain color. Anything that you could test with TDD, wondering if you can somehow apply proofs. If so, how.

up vote 8 down vote accepted

Tests are not proofs. Tests are experiments. Proofs are formal arguments. But both can be used to decide a proposition (a statement that may be true or false). In general, our propositions have the form “∀x: p(x)” (for all inputs/examples x, some property p holds).

Tests/experiments only try out specific examples. They do not in general cover every alternative. So strictly speaking, they don't show that a property always holds, only that this property is possible: “∃x: p(x)”. The reverse case is much more interesting: if an example fails, this disproves our hypothesis.

We can therefore say that testing places a maximum bound on correctness: we can show where the system is incorrect by finding failing test cases.

To construct a proof of correctness, we need to formalize relevant aspects of the semantics of the program, and formally define what “correct” means. This is extremely tricky, because such systems quickly become unwieldy. In particular, if our formal system is too expressive, it may become undecidable. This is similar to the constraints on symbolic execution, which could be seen as one proof technique. Formal techniques are then only useful to discuss certain properties of a program, but are generally unable to prove “correctness” in its entirety.

We can therefore say that formal proofs place a minimum bound on correctness: we may be able to prove some basic properties of the program, but usually not all interesting properties.

Because proofs are tedious they are generally only used when they can be automated. In the context of programming languages, type systems provide a formal system that can be decided automatically (though many real-world type systems are undecidable and/or unsound). Type systems generally describe what we can do with values, e.g. which methods are available on some object.

Some type systems also include an effects system, where effects formalize properties that are not bound to values. An effect connected to a function type could be that the function throws an exception, never returns, represents a coroutine that yields, or performs I/O (or many other effects). Haskell is the only common language that uses an effects system for I/O, via the IO monad. However, this only shows whether I/O is possible (it cannot generally be used to show that I/O has happened), and of course the Haskell type system is technically unsound (any function could call unsafePerformIO).

Proving that a program will produce output is extremely tricky. Your test case simplifies this problem to showing that a certain output-producing function is called instead (console.log). These properties are not equivalent. In fact, your test proves (!) that your log function does not always produce output, because it doesn't write anything to the console when used in your test. (Proving anything of interest in dynamic languages like JS or Python is super tricky, unless you take extra steps to nail down the code. Here, creating an immutable binding to console.log like var log = (function(console_log){ return function log(a) { console_log(a) })(console.log) would help.)

Instead of considering such special cases, we could write a proof that ignores these cases, by choosing convenient assumptions or formal systems. For example:

Assumptions:

  • (1) Let console.log be a function that takes one argument of any type and prints a representation of the value of that argument.
  • (2) Let log be a function that takes one argument a of any type, calls console.log with a exactly once, and returns the undefined object.

Proposition: For all values x, when log is called with that value, it prints a representation of that value.

Proof:

  • When log is called with x, then it follows from (2) that console.log is called once with x.
  • When console.log is called with x, then it follows from (1) that it prints a representation of x. ∎

This was an extremely simple proof where the proof basically just consisted of rephrasing the (carefully chosen) assumptions. Similar to “Let a = b and b = c. Proposition: a = c”. This also means such proofs don't have any practical value.

Practical proofs often cover propositions such as: does this loop/recursion terminate? Does this function run in O(n) time? Is this function guaranteed to never throw? Is a certain action performed at most once for each input?

There are some further connections between proofs and tests in software QA:

Experiments can be seen as supporting the truth of our “∀x: p(x)” argument by inductive reasoning (generalization). For example, dividing test input into equivalence classes lets us test a single example from each class. We can then generalize that we would get the same result for all members of that class. This works fine as long as the class does in fact behave equivalently. We might want to formally prove that.

A related strategy is property-based testing. Instead of choosing specific examples for our test cases (p(1) ∧ p(2) ∧ ⋯) we keep our test cases parametrized so that they describe the proposition p. We then use some software that chooses random examples. This reduces the influence of our biases when creating equivalence classes, thus supporting an inductive argument for correctness.

But again: supporting evidence is not the same as a proof. Generalization is practically useful, but always comes with some risk of errors.

  • Wow this is excellent, thank you! – Lance Pollard May 21 at 15:16
  • "such proofs don't have any practical value" that's what I kept thinking, yay! Now starting to see. "Practical proofs often cover propositions such as..." good stuff – Lance Pollard May 21 at 15:17
  • Ooh ooh, wondering what the proof would look like for this log function with "Is this function guaranteed to never throw?" – Lance Pollard May 21 at 15:19
  • Anyway, very helpful answer :) – Lance Pollard May 21 at 15:21
  • @Lance The proof for “log never throws” would be enumerating all expressions that can throw, and proving that none of them can happen. Here, we'd have to show that console.log is a function that never throws when called with one argument (either accessing the value console.log could throw, or calling that value, or the code in the function). – amon May 21 at 16:00

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.