Eiffel10: An object-oriented language with dynamic frame contracts
Bernd Schoeller · Repository for Publications and Research Data (ETH Zurich) · 2006
The purpose of this document is to define a very small language Eiffel0 as a subset of Eiffel[1]. The definition comes with a heap model and an operational semantics of the execution of Eiffel0 programs within the heap. Eiffel0 is a subset of Eiffel. It main purpose is to explore reasoning about reference structures, aliasing