Automating NULL check contracts

[sonntag benoit]

Mildred Ki'Lya <ml.mildred593 at gmail.com> a écrit :

> Content-Type: text/plain; charset=UTF-8
> Content-Transfer-Encoding: quoted-printable
>
> Hi,
>
> (french translation afterwards)
>
> In my experience, most of the bugs comes from a call on NULL.
> (I'm writing this because I found a call on NULL in the compiler)
>
> Now, ideally, a good programmer should write contracts like this:
>
>   - my_slot arg2:TYPE keyword arg2:TYPE :TYPE <-
>   [
>     -? {arg1 != NULL};
>     -? {arg2 != NULL};
>   ]
>   (
>     ... // Implementation
>   )
>   [
>     +? { Result != NULL };
>   ];
>
> But now, in this ideal world, we add good programmers.
> By definition, good programmers are lazy.
> And good programmers don't want to write these contracts each time they
> define a slot for the first time (thankfully, assertions are inherited).
>
> So, instead of crashing on an assertion (the closest to the error) we
> crash on the call on NULL.
>
>
> Now, Bertrang Meyer's version of Eiffel have something to avoid calls on
> NULL:
> http://bertrandmeyer.com/2009/08/04/void-safety-getting-rid-of-the-spectre-of-null-pointer-dereferencing/
> http://docs.eiffel.com/sites/default/files/void-safe-eiffel.pdf
>
>
> We could also imagine something that will automatically write contracts
> to check NULL values.
> Here I see two problems:
>
>     * if we create an external tool that rewrite the source code, how do
>       you tell where to check for NULL and where NULl might be legitimate
>     * if it is included in the Lisaac compiler, how to make it work (the
>       ?{} construction is implemented in the library)
>
>
>
>
> Now, do you have any ideas?
>
> ------------------------------------------------------------------------
>
> Dans mon expérience, la plupart des bugs sont causés par des appels sur
> NULL (call on NULL)
> (j'en parle maintenant parce que j'ai justement un call on NULL dans le
> compilateur)
>
> Idéalement, un programmeur devrait écrire:
>
>   - my_slot arg2:TYPE keyword arg2:TYPE :TYPE <-
>   [
>     -? {arg1 != NULL};
>     -? {arg2 != NULL};
>   ]
>   (
>     ... // Implementation
>   )
>   [
>     +? { Result != NULL };
>   ];
>
> Dans ce monde idéal, ajouton de bons programmeurs
> Les bons programmeurs par définition sont fainéants
> Donc, un bon programmeur n'écrire pas ces contrats à chaque fois qu'ils
> définissent un nouveau slot (heureusement, les contrats sont hérités).
>
> Au lieu de planter sur une assertion (au plus près de l'erreur), on
> plante donc sur un appel sur NULL.
>
>
> La version d'Eiffel de Bertrand Meyer a corrigé ce problème pour éviter
> tout appel sur NULL:
> http://bertrandmeyer.com/2009/08/04/void-safety-getting-rid-of-the-spectre-of-null-pointer-dereferencing/
> http://docs.eiffel.com/sites/default/files/void-safe-eiffel.pdf
>
>
> On peut imaginer quelque chose dans le même goût, ou on pourrait
> imaginer quelque chose qui écrirait ces contrats à notre place pour
> vérifier les valeurs NULL. Mais je vois deux problèmes:
>
>     * Si on crée un outil extérieur qui va réécrire le code source,
>       comment savoir où placer ces contrats (et où les valeurs NULL sont
>       légitimes)?
>     * Si c'est inclus dans le compilateur, je vois mal comment faire,
>       sachant que la construction ?{} est implémentée en lib.
>
> Maintenant, avez vous des idées ?
>

Article OOPSLA 2007 :
Title :
"Tracking bad apples: reporting the origin of null and undefined value errors"

This article is really interesting for your pb.
And the solution is simple to set up.

No ?

Ben.


> Mildred
>
> --
> Mildred Ki'Lya
> ?????????? ???????????????????? ??????????
> ? Jabber, GoogleTalk: <mildred at jabber.fr>
> ? Website: <http://ki.lya.online.fr>           GPG ID: 9A7D 2E2B
> ? Fingerprint: 197C A7E6 645B 4299 6D37 684B 6F9D A8D6 9A7D 2E2B
>
>