Description:
The object-oriented Eiffel language.
|
|
|
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 »
|
|
|
Type safe Eiffel
|
| |
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... more »
|
|
|
Finally eiffelstudio w/ SCOOP: HELP!
|
| |
Hello all, Now Eiffel SCOOP is supported by eiffelstudio, but I do not know how to use it! I have two classes in my program: class PF_HP -- -- The "Proteinfolding in HP-Model" for Eiffel :-) -- -- To compile type command : ec -config pf_hp.ecf -- Run with command : ./pf_hp -- --... more »
|
|
|
EiffelStudio: big .EXE file size
|
| |
I tryed the last EiffelStudio on Windows Vista with MinGW: "Hello world" program (.EXE file) is about 24Mb!! Does it possible to optimize the size, some way to shrink generated .exe?.. /Pavel
|
|
|
