Automating NULL check contracts

[Mildred Ki'Lya]

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 ?

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.alioth.debian.org/pipermail/lisaac-devel/attachments/20090930/5d051ce7/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 197 bytes
Desc: OpenPGP digital signature
URL: <http://lists.alioth.debian.org/pipermail/lisaac-devel/attachments/20090930/5d051ce7/attachment.pgp>