Difference between revisions of "EiffelBase2"

(New page: Category:Library This page is under construction. It will contain a description of the EiffelBase2 library: a general purpose data structures library for Eiffel designed for formal sp...)
 
(Basic information)
Line 1: Line 1:
 
[[Category:Library]]
 
[[Category:Library]]
  
This page is under construction.
+
==Overview==
It will contain a description of the EiffelBase2 library: a general purpose data structures library for Eiffel designed for formal specification and verification.
+
 
 +
EiffelBase2, currently under development, is a general-purpose data structures library for Eiffel. It is intended as the future replacement for the [[EiffelBase]] library ("Classic EiffelBase" in this document), which has for many years played a central role in Eiffel development.
 +
 
 +
==Design goals==
 +
 
 +
The design goals for EiffelBase2 are:
 +
 
 +
*Verifiability. The library is designed to allow proofs of correctness.
 +
 
 +
*Full contracts. Partly as a result of the verifiability goal, but also for clarity and documentation, the contracts associated with classes and features should describe the relevant semantics in its entirety.
 +
 
 +
*Simple and consistent hierarchy, in particular avoidance of descendant hiding and of "taxomania" (classes not representing a meaningful abstraction, unnecessary inheritance links).
 +
 
 +
*As in Classic EiffelBase, application of a systematic classification (a theory) of fundamental data structures.
 +
 
 +
*Full traversal mechanisms, based on external cursors (with internal cursors also provided when useful).
 +
 
 +
*Client-interface compatibility with corresponding classes in Classic EiffelBase, whenever it does not conflict with he preceding goals.
 +
 
 +
==Status==
 +
 
 +
Development of EiffelBase has started as a project at ETH Zurich; see the [http://eiffelbase2.origo.ethz.ch/ project page]. Documentation and other material will soon be transferred to the present page.

Revision as of 05:32, 17 April 2010


Overview

EiffelBase2, currently under development, is a general-purpose data structures library for Eiffel. It is intended as the future replacement for the EiffelBase library ("Classic EiffelBase" in this document), which has for many years played a central role in Eiffel development.

Design goals

The design goals for EiffelBase2 are:

  • Verifiability. The library is designed to allow proofs of correctness.
  • Full contracts. Partly as a result of the verifiability goal, but also for clarity and documentation, the contracts associated with classes and features should describe the relevant semantics in its entirety.
  • Simple and consistent hierarchy, in particular avoidance of descendant hiding and of "taxomania" (classes not representing a meaningful abstraction, unnecessary inheritance links).
  • As in Classic EiffelBase, application of a systematic classification (a theory) of fundamental data structures.
  • Full traversal mechanisms, based on external cursors (with internal cursors also provided when useful).
  • Client-interface compatibility with corresponding classes in Classic EiffelBase, whenever it does not conflict with he preceding goals.

Status

Development of EiffelBase has started as a project at ETH Zurich; see the project page. Documentation and other material will soon be transferred to the present page.