Type of project:
Semesterarbeit SS 2007
Complete Contracts for EiffelBase
This semester thesis is an effort to redevelop a major part of the Eiffel Base Library to support Dynamic Frame Contracts and Models. The goal is to redesign and implement as much as possible in the given time-frame, with a focus is on the implementation of the linked list class in the Eiffel Base Library and all supporting classes. The purpose of using Dynamic Frame Contracts and Models is to allow full functional specifications and therefore formal verification.