| Sumario: | In computer science dealing with non denoting terms is a common occurrence. In the programming language Eiffel, if a term does not denote an object, it is an alias of Void. In introducing Void into his programming language, Algol W, Hoare considers it his billion dollar mistake. To mitigate the errors in using Void, the programming language Eiffel has introduced a Void-Safety mechanism. This mechanism makes explicit the presupposition of the existence of terms. In the following article the logic of assertions in Eiffel is considered not a standard logic due to the use of Void, but a Free Logic. This has implications for the correctness of programs.
|
|---|