Re: [Caml-list] About "precise (formal) things that can be said about properties of certain interfaces"

[Jesper Louis Andersen <jesper.louis.andersen@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2168 bytes --]

On Tue, Jun 21, 2016 at 9:11 PM, Gabriel Scherer <gabriel.scherer@gmail.com>
wrote:

> In my experience, this is an excellent mindset in which to put code
> authors at the moment they are designing and implementing the function (so
> these tests should come simultaneously, not after the implementation
> effort), because it makes you think about the properties the function
> should have, and this is a very effective way to make the right choices on
> corner cases: most choices will *not* respect nice properties, and those
> that do are the right ones.


Elaborating with an insight I once learned from John Hughes.

When a QuickCheck test case fails, one out of three things are wrong. They
are wrong with about the same frequency:

1. The system-under-test has a failure
2. The property/test specification has a failure
3. The generator, producing random inputs has a failure.

If the 1st happens, it is a genuine bug which can be fixed. If the 2nd
happens, it forces you to think about and strengthen the property, which
after a couple of rounds of strenghtening often results in the 1st case.
The 3rd case is peculiar since it tells you something about the (input)
domain, which often is as important as the property themselves.

A war story was a circuit breaker system I wrote for Erlang. In this
system, there was a specific configuration parameter which could be any
natural number (including 0). But it turned out there were lots of failures
when the configuration parameter was 0. This forced me to think, and I soon
realized that a parameter of 0 did not make any sense, so I changed the
validity domain to be 1 or greater, and added a test which made sure that 0
or less would return an error on system setup.

But then, the code coverage showed a lot of dead code. It turned out my
code had two code paths through it: the 0 case, and everything else. And
the 0 case didn't work. I ended up deleting about half of that module as a
result. QuickCheck systems are really good at testing your boundary and
edge cases for correctness. A really good QC implementation could perhaps
even find that OCaml's default List.map is not tail recursive :)



-- 
J.

[-- Attachment #2: Type: text/html, Size: 2948 bytes --]