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.

Create a free website or blog at