Some months ago I have started a blog about static verification of software.

The blog already contains a significant amount or articles like "Functions, ghost functions and higher order functions", "Framing: An approach to mutability", "Introduction to the proof engine", "Proof procedures" etc.

For those of you who are interested in this topic, you can check it out at http://softwareverifica

From the beginning of Eiffel the language has been characterized as strongly typed. But since its beginning there has been a hole in the type system which has not yet been fixed up to now (the so called catcall problem).

What is the hole?

The existence of the hole can be demonstrated with very simple examples.

From the beginning of Eiffel the language has been characterized as strongly typed. But since its beginning there has been a hole in the type system which has not yet been fixed up to now (the so called catcall problem).

What is the hole?

The existence of the hole can be demonstrated with very simple examples.

From the beginning of Eiffel the language has been characterized as strongly typed. But since its beginning there has been a hole in the type system which has not yet been fixed up to now (the so called catcall problem).

What is the hole?

The existence of the hole can be demonstrated with very simple examples.

From the beginning of Eiffel the language has been characterized as strongly typed. But since its beginning there has been a hole in the type system which has not yet been fixed up to now (the so called catcall problem).

What is the hole?

The existence of the hole can be demonstrated with very simple examples.

From the beginning of Eiffel the language has been characterized as strongly typed. But since its beginning there has been a hole in the type system which has not yet been fixed up to now (the so called catcall problem).

What is the hole?

The existence of the hole can be demonstrated with very simple examples.

In Eiffel all arguments of routines are pure input arguments. There is no possibility to return an argument. The only possibility is to write a function and return a value as "Result".

Furthermore Eiffel has command query separation, i.e. a command can change states and a query should only return a result and do nothing beside that.

The following is a short description of a solution to the catcall problem (recently posted in comp.lang.eiffel as well):

In Eiffel it is easy to generate runtime type errors. Therefore Eiffel cannot (yet) be considered to be a typesafe language.

Main features of Eiffel

The main features of Eiffel are:

- clean object orientation with multiple inheritance

- design by contract

- elegant expressive syntax

- automatic memory management

- generics

- uniform type system with type safety (exept catcalls)

These features were unique at the time Eiffel was invented (some 25 years ago).

The Eiffel language in its current definition has no concept of namespaces. However in large programs using many libraries name clashes (i.e. two classes having the same name) become more and more probable.

Different Eiffel compilers have resolved the name clashes with different strategies. This is not satisfactory because it is not portable.