From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id ACD4A7FA5C for ; Tue, 21 Jun 2016 22:07:13 +0200 (CEST) IronPort-PHdr: 9a23:JRk/yBLX8qiCYpLbu9mcpTZWNBhigK39O0sv0rFitYgVKvjxwZ3uMQTl6Ol3ixeRBMOAuqoC07Kd4/6ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD14Lvj6vipdX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DbKRxGO639UaW4WnwBFGUCR4xjwRJb8tm3hvepwwiSAFcLzRLEwHz+l6vE4ZgXvjXIlOiUh/XufrsttjbkTiRStqgZkzoicNIOYL+JzZOXZes4bXixIWMpcTTdMBKuzaoIOC6wKOuMO/Nq1nEcHsRbrXVrkP+jo0DIdwyauhaA= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jesper.louis.andersen@gmail.com; spf=Pass smtp.mailfrom=jesper.louis.andersen@gmail.com; spf=None smtp.helo=postmaster@mail-lf0-f44.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jesper.louis.andersen@gmail.com) identity=pra; client-ip=209.85.215.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jesper.louis.andersen@gmail.com"; x-sender="jesper.louis.andersen@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jesper.louis.andersen@gmail.com designates 209.85.215.44 as permitted sender) identity=mailfrom; client-ip=209.85.215.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jesper.louis.andersen@gmail.com"; x-sender="jesper.louis.andersen@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-lf0-f44.google.com) identity=helo; client-ip=209.85.215.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jesper.louis.andersen@gmail.com"; x-sender="postmaster@mail-lf0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DTAACKnWlXhizXVdFdg1yBNQaoAo1uhQGBeoYXAoEuBzgUAQEBAQEBAQERAQEBCAsLCSEvgjGCGwEBAwESER0BGx0BAwELBgUEBzAHAgIhAQERAQUBHAYTIodzAQMPCKRfgTE+MYs7gWqCWQWHNQoZJw1SgyMBAQEBBgEBAQEBGgIGEIpkgkOEfoJaAQSYRTSMMoF6jyOIC4YuEh6BDx6CMQ0RCxeBNzoyikgBAQE X-IPAS-Result: A0DTAACKnWlXhizXVdFdg1yBNQaoAo1uhQGBeoYXAoEuBzgUAQEBAQEBAQERAQEBCAsLCSEvgjGCGwEBAwESER0BGx0BAwELBgUEBzAHAgIhAQERAQUBHAYTIodzAQMPCKRfgTE+MYs7gWqCWQWHNQoZJw1SgyMBAQEBBgEBAQEBGgIGEIpkgkOEfoJaAQSYRTSMMoF6jyOIC4YuEh6BDx6CMQ0RCxeBNzoyikgBAQE X-IronPort-AV: E=Sophos;i="5.26,506,1459807200"; d="scan'208,217";a="223354747" Received: from mail-lf0-f44.google.com ([209.85.215.44]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Jun 2016 22:07:12 +0200 Received: by mail-lf0-f44.google.com with SMTP id h129so41220861lfh.1 for ; Tue, 21 Jun 2016 13:07:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=4DUiR3RVfrxaYZIhI3fs5uEWhr6gaX8Iu+THbQLp+gs=; b=lJ4ZGjt+7zAZrsSeD63ZDT3fAYy4BTERK4HrR2z3DMve9fJnOEjpvo8DFXBlXsGcYo QiYKXxX1lOG0jfHq1fy+xjoX1l873PfmR3/NYa81FerOhM6m7QfdQviWoNMEe74JhlLO wmItW345mQR1JS+lQI9VRQlW4CDKDgGt9dEjWgP/EKlTX2cyRERE1kxdkZfL+1zAvNJE FyZkafd750p7M7DAcZTxjHVUTDZ8oZeJZMoysVJucaz2dqT5O4ycSaKOVxbC6OXUQmID V8C7Xc2NXUeJBe5Mqe94ZQ+yhDshtB/4tIEDzMB+n0hIP7D5fyGZnhsAa228Bg9HelpB 0DYw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=4DUiR3RVfrxaYZIhI3fs5uEWhr6gaX8Iu+THbQLp+gs=; b=TNSWihWMzD2WyWLKfujJfwYVMxH41GdJqbzErCQ9I/VCpmlzs+niIusBewUrJfvdnj ZIIMjf2ChQBzopZN69qwv9jCN+Emil/67J3hDF9h7e3K2aqPo5deDvqDRnCbWeFAfRRN /c6lEMSnVYiq3EE98GUwciuFe94lIUD7b4ODNrPztXRSY/OWiBylS3AioCiYXjiUo6NE 8ZGD7vcYVXjfxOYeqc5u88fNZ012AHsau4CwzJzVxHTajtelngL4ZqKJhs/f9ILl5/5i 2u/csYsov+NPhkznY5xpee/VMwAl2PRb30i/512d/Z/m9p4Jt+ISx1ZCiXwVDvpDpydC sjlw== X-Gm-Message-State: ALyK8tIY9zvnt23qH3jZbfrasPz3ZIvl1LqdQSpqXE+vfP2HnMsMTebFPXB/Etr8ZywsvAiBs4tLSayV26KH4g== X-Received: by 10.25.146.209 with SMTP id u200mr5152607lfd.224.1466539632218; Tue, 21 Jun 2016 13:07:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.155.135 with HTTP; Tue, 21 Jun 2016 13:06:32 -0700 (PDT) In-Reply-To: References: <5E818FB5-6908-4E29-838E-C6A2836F60CE@inria.fr> <25b304ab-c9ea-ff68-2059-68c93683b1a2@linux-france.org> From: Jesper Louis Andersen Date: Tue, 21 Jun 2016 22:06:32 +0200 Message-ID: To: Gabriel Scherer Cc: David MENTRE , caml users Content-Type: multipart/alternative; boundary=001a11401508d3d8a50535cf5d94 Subject: Re: [Caml-list] About "precise (formal) things that can be said about properties of certain interfaces" --001a11401508d3d8a50535cf5d94 Content-Type: text/plain; charset=UTF-8 On Tue, Jun 21, 2016 at 9:11 PM, Gabriel Scherer 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. --001a11401508d3d8a50535cf5d94 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

= On Tue, Jun 21, 2016 at 9:11 PM, Gabriel Scherer <gabriel.scherer@= gmail.com> wrote:
In my ex= perience, this is an excellent mindset in which to put code authors at the = moment they are designing and implementing the function (so these tests sho= uld come simultaneously, not after the implementation effort), because it m= akes 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.<= /blockquote>

Elaborating with an insight I once learned from John = Hughes.

When a QuickCheck test case fails, one out of three things are wrong. The= y are wrong with about the same frequency:
=
1. The system-under-test has a failure=
2. The property/test specification has a f= ailure
3. The generator, producing random i= nputs 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 prope= rty, which after a couple of rounds of strenghtening often results in the 1= st case. The 3rd case is peculiar since it tells you something about the (i= nput) domain, which often is as important as the property themselves.
A war story was a circuit breaker system I wrote for Erlang. In this syst= em, there was a specific configuration parameter which could be any natural= number (including 0). But it turned out there were lots of failures when t= he configuration parameter was 0. This forced me to think, and I soon reali= zed 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 ca= se, and everything else. And the 0 case didn't work. I ended up deletin= g 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.
--001a11401508d3d8a50535cf5d94--