Mohsen Vakilian's Blog

April 14, 2010

Void Safety in Eiffel

Filed under: language — mohsenvakilian @ 12:20 pm

In a QCon 2009 talk, Tony Hoare called the invention of the null reference in 1965 his billion-dollar mistake.

Dereferencing null objects is known as the void safety problem. Bertrand Meyer et al. describe how they’ve added void safety to Eiffel in the paper “Avoid a Void: The eradication of null dereferencing“.

The authors argue that attempts to remove Void completely fail because there are valid uses of it. Moreover, they claim that terminating linked structures seem to be the only case that truly requires void references.

They implement a static type checker that ensures void safety for Eiffel. The main rule that the static type checker enforces is that a call x.f(...) is permitted only if x is statically attached. An attached type does not admit Void as one of its values.

They’ve developed straightforward rules to enforce preservation of the attachment property through assignment and argument passing.

To make the void safety mechanism easier to use, the type checkers infers non-void values in certain contexts. For example, if x is a local variable, the call in if x /= Void then x.f(...) is void-safe. However, if x is not a local variable, the call is no longer guaranteed to be void-safe because of the possibility of side effects in a multithreaded environment. In such cases, we need to use object tests. The object test in the statement if attached x as l then l.f(...) end checks that x is dynamically attached to an object. Then, it binds x it to the local name l. The scope of l in this case is the then clause.

Eiffel has a Check instruction which is a kind of assert statement. The paper suggests to use this instruction to limit the use of explicit object tests. But, one has to write an object test when using the Check instruction. So, I don’t see how the Check instruction replaces object tests. I’d guess that what they mean by limiting object tests is the number of object tests performed at runtime. According to the semantics of the Check instruction, if the compiler proves that the object test always succeeds, we won’t perform the test at runtime.

The paper also proposes stable attributes as a way of reducing the number of object tests. Stable attributes are defined as the following.

A detachable attribute is stable if it does not appear as the target of an assignment whose source is a detachable expression.

The paper mentions that the compiler can check the stability of an attribute by just checking the assignments in the class. I’m not familiar with Eiffel. And, it’s not clear to me how the compiler handles assignments outside the class.

The paper extends the void safety mechanism to generic types. But, they treat arrays specially because elements of an array don’t get initialized when the array is created. So, they introduce a new constructor for array that fills the array by a given initial value.

Finally, the paper reports on the conversion effort for making Eiffel code void-safe. The percentages of lines changed in EiffelBase and EiffelVision were about 11% and 3%, respectively. These figures confirm that making system-level libraries void-safe takes much more effort than user applications.

Advertisements

2 Comments »

  1. “I’d guess that what they mean by limiting object tests is the number of object tests performed at runtime.”
    Indeed, all assertions (check clause, preconditions, postconditions, class invariant) can be disabled for better performance.

    “The paper mentions that the compiler can check the stability of an attribute by just checking the assignments in the class. I’m not familiar with Eiffel. And, it’s not clear to me how the compiler handles assignments outside the class.”
    In Eiffel a class argument is only changeable with a command (modifier) call.

    Comment by Victorien ELVINGERonaclos — August 18, 2013 @ 5:11 pm | Reply

  2. […] void instead of null). For more information search for ‘eiffel void safety’, refer to a quick overview or chapter Void-safe programming in Eiffel in the official […]

    Pingback by Why we should Love ‘null’ | Windows 8 Blog — July 31, 2014 @ 10:54 am | Reply


RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Blog at WordPress.com.

%d bloggers like this: