Description:
The object-oriented Eiffel language.
|
|
|
Command line compilation
|
| |
Dear Eiffel enthusiasts,
My task is to develop a website on which students can type Eiffel classes (plain .e-files), click a button and compile what they just have typed.
For that I which to address the command line Eiffel compiler (ec.exe).
How do I execute this compiler so that
- The right class is used as the root class.... more »
|
|
|
Old books about Eiffel - anyone interested?
|
| |
I'm clearing out some old Eiffel books. If anyone wants them, I'm asking for five bucks each plus the actual postage cost (depending on where you live). Mailing from the UK.
Even the books without "Eiffel" in their title are indeed focused on Eiffel. For a while some authors tried to broaden their potential market by not mentioning Eiffel on the front cover.... more »
|
|
|
Nexus Programming Language
|
| |
The Nexus programming language version 0.5.0 has been released. It is
an "object-oriented, dynamically-typed, reflective programming
language", drawing from Lua and Ruby. [link]
|
|
|
Reasoning with quantified expressions in predicate calculus
|
| |
In order to prove software to be correct, predicate calculus with
quantified expressions (for all, exists) is indispensable. The
programming language Modern Eiffel has all possibilities to do
predicate calculus.
The article
[link]
describes how reasoning with quantified expressions is done in Modern... more »
|
|
|
Reasoning with inductive types
|
| |
Modern Eiffel is a new language which is syntactically based on Eiffel
but has a lot of concepts of functional languages like Haskell, OCaml
or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a
compiler can statically check that a programm written in Modern Eiffel
meets its specification.... more »
|
|
|
Negation and proofs by contradiction
|
| |
A new blog entry [link]
has beed created with continues the description of Modern Eiffel's
proof engine.
This blog entry focuses on the introduction of negation and it's
axioms into the class BOOLEAN and presents a rich set of proofs.... more »
|
|
|
SW Verification with (Modern) Eiffel
|
| |
I have started a blog to talk about SW verification. In this blog I
use a variant of Eiffel called "Modern Eiffel". The latest blog entry
at [link]
gives an outline of the language. It describes the use of inductive
data types (or sometimes called algebraic data types) within Modern... more »
|
|
|
Tumia the first Object-Oriented Internet Directory
|
| |
Hi,
To my knowledge Tumia ([link]) is the first internet
directory structured according to the object-oriented paradigm.
Currently Tumia is in its baby years. To illustrate the object-
oriented concept consider below "Navigate from Earth Global Warming
2000 AD to Mitigating Solar Energy and Back" which is a specific... more »
|
|
|
correctness proofs demonstrated with natural numbers
|
| |
I have written a paper to show how natural numbers without any conceptual limitation (i.e. arbitrarily sized) can be implemented and verified in Modern Eiffel. The fact that the implementation is highly inefficient to execute is accepted. The implementation shall serve as a model on how to implement inductively defined... more »
|
|
|
