The Eiffel Compiler / Interpreter (tecomp)

3.12.2012

Modern Eiffel goes concurrent!

I have started a new series of papers describing concurrency in Modern Eiffel.

The first one An introduction to processes gives an overview on how processes will be treated in the programming language.

Furthermore some more papers are available as well.

- Binary relations, endorelations and transitive closures
- Functions and complete partial orders
- Closures and fixpoints

16.9.2012

A lot more papers are now available to describe the specification power of Modern Eiffel.

- Predicates, ghost predicates and higher order predicates
- Oder structures: abstraction and multiple inheritance
- Lattices: Partial orders with infimum and supremum
- An approach to framing and mutability
- The implementation side of framing
- The insertion sort algorithm
- The heapsort algorithm
- Boolean lattices (i.e. boolean algebras)
- Predicates as sets
- Complete lattices and closure systems

28.4.2012:

A couple of papers have been written to explore the properties of Modern Eiffel

- Resoning with inductive types
- Resoning with quantified expressions
- Specification and implementation of modules
- Tuples and functions
- Ghost functions and higher order functions
- Simple examples of inheritance
- Proofs as programs(proof procedures)

I will continue to write more articles to describe Modern Eiffel more in detail before I start with the implementation. It is worthwhile to do this and not to make a quickshot implementation.

In the course of writing these articles some needed changes became evident.

During the work on Specification and implementation of modules it became evident, that there is a need to take functions and procedures out of the class declaration and put them into the module declaration. This keeps all the expressive power of object orientation and reconciles object orientation with functional programming.

During the work on Proofs as programs(proof procedures) a better interface to the proof engine in the form of proof procedures have been explored. Proof procedures might be a better and easier to grasp interface to the proof engine than proof commands. This option will be explored in the coming articles.

24.2.2012:

A description of negation and proofs by contradiction has been added as a white paper. This paper demonstrates how Modern Eiffel's proof engine can be used to make proofs by contradiction.

19.2.2012:

An introduction of the proof engine has been added to the white papers.

25.1.2012:

A series of blog entries have been started to describe how Modern Eiffel can be used to write correct SW. The first blog entry describes the outline of the language with special emphasis on immutable and inductive types (doc/papers/proof/lang_outline.txt).

14.8.2011:

The concept of the proof engine in Modern Eiffel is progressing well. In order to get a feeling of the capabilities of the proof engine the paper doc/papers/proof/math_nat.pdf has been written. It describes the implementation of natural numbers without any conceptual limitation in Modern Eiffel and shows the proofs which can be derived by the proof engine automatically. The implemented natural numbers are highly inefficient to executed. The purpose is not to execute them, the purpose is to demonstrate Modern Eiffel's capabilities for modelling and verification.

16.6.2011:

Type features are available in Modern Eiffel. They allow to define a family of types which redefine features covariantly in a typesafe manner. They can be used to define parallel hierachies and are similar to path dependent types of Scala.

5.6.2011:

Universal conformance has been integrated into Modern Eiffel. Modern Eiffel now reconciles type safety and universal conformance (see doc/papers/lang/modern_eiffel.txt).

10.5.2011:

The concept for a verifying compiler is progressing well. The concept of the proof engine has been improved significantly. It can now do much more proofs automatically than before . It can expand definitions including recursive definitions (only one level) even if the resulting assertions are more complicated than the original. A paper will be published soon.

The framing problem has been solved. There is no need that the user enters framing conditions in features like "modify" or "use". The assertions are expressive enough to state what a feature uses and modifies.

Currently the concept will be extended to include concurrency (i.e. correctness proofs like absence of dead and lifelocks etc.). This is ongoing activity.

No implementation is currently done, because the concept needs to stabilize and needs to include concurrency.

17.3.2011:

Parallel wait has been added to the draft specification of Modern Eiffel

15.3.2011:

A draft description of Modern Eiffel has been published http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/modern_eiffel.txt.

Modern Eiffel has been designed to overcome the shortcomings of Classic Eiffel in order to reach

- full type safety
- static verification of assertions
- powerful concurrency

13.3.2011:

In the last year there were only two releases of The Eiffel Compiler. This might make the impression that there is little activity in the project. But this is not the case. A lot of conceptual work happened in the background.

The need of the conceptual work has been: Classic Eiffel has some shortcomings which need to be overcome for the needs of the tecomp project. Two of the major goals of the tecomp project are:

- Create a compiler which can statically verify assertions (i.e. a proving compiler).
- Create a compiler which has support of concurrency in a manner which avoids race conditions, deadlocks (or at least detect them statically or at runtime).

Both goals cannot be achieved without modifying Classic Eiffel in some areas. At the start of the tecomp project the ECMA standard seemed to be a good basis to work with but a deeper analysis uncovered that ECMA Eiffel has nearly the same shortcomings as Classic Eiffel.

After one year of conceptual work it can be said that the definition of a Modern Eiffel is converging. This is an evolution of Classic Eiffels which avoids the above mentioned shortcomings. A white paper describing Modern Eiffel will be published soon.