\chapter*{Abstract}
\label{sec:Abstract}
\addcontentsline{toc}{chapter}{Abstract}

Formal verification of programs is a very important topic. But on the other hand it is rather difficult to be able to verify a program if only the source code is given. Using Eiffel, not only the code itself can be used but also contracts. Each feature has preconditions and postconditions which can be used to enhance and simplify the verification process. But unfortunately the contracts currently used in Eiffel are under-specifications in the sense that there are always some properties when invoking Eiffel features that are not expressed through its contracts. To be able to write complete contracts, Dynamic Frame Contracts are added for each feature and Models are used to enhance existing contracts.

In this semester thesis, we try to redevelop a major part of the EiffelBase Library to support Dynamic Frames and Models. A focus is on the LINKED\_LIST class and all its supporting classes to allow full functional specifications and therefore formal verification.
