Abstract
This lecture note explains how contracts can be written to express properties of entire data structures, when methods mutate the contents of those structures.
We will see two mechanisms that serve this purpose: Immutable lists, which are derived from functional programming concepts and are used to express data structure contracts in Eiffel, and shallow copies, which are used in many modern contract development tools such as JML and MS Code Contracts. Examples are provided in JML.
We will see two mechanisms that serve this purpose: Immutable lists, which are derived from functional programming concepts and are used to express data structure contracts in Eiffel, and shallow copies, which are used in many modern contract development tools such as JML and MS Code Contracts. Examples are provided in JML.
| Originalsprog | Engelsk |
|---|---|
| Publikationsdato | 2016 |
| Antal sider | 9 |
| Status | Udgivet - 2016 |