Automating NULL check contracts

[Mildred Ki'Lya]

More explanations ...
(french translation afterwards)

On 09/30/2009 06:05 PM, Mildred Ki'Lya wrote:
> 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
>

The main idea in this paper is that types can be either attached or
detached (a keyword specifies this)

Variables with unattached types can contain NULL values. This is the
default for most languages.

Variables having an attached types are not allowed to contain NULL. This
is checked at compile time by ensuring that these variables cannot be
affected with unattached expression. If you want to affect them with
unattached expressions, you have to check for NULL before.

Now, the compiler can give you an error when you try to call a slot on
an unattached variables because this may be a cause of call on 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
>

L'idée principale de ce papier c'est qu'un type peux être soit attaché
ou détaché (un mot chef est rajouté au langage).

Les variables avec un type détaché peuvent contenir des valeurs NULL.
C'est le cas par défaut pour la majorité des langages.

Les variables avec un type attaché ne sont pas autorisées à contenir des
valeurs NULL. C'est vérifié au moment de la compilation. Le compilateur
vérifie que ces variables ne peuvent pas être affectées par des
expression de type détaché. Si on veut tout de même faire une
affectation, on doit vérifier que l'expression n'est pas NULL avant.

Cela permet au compilateur de signaler une erreur lorsqu'il y a un appel
sur un type détaché, car il est la cause potentielle de crash "call on
NULL".

-- 
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/6c5c0c7f/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/6c5c0c7f/attachment.pgp>