Contract-Based Software Development: Immutable Lists and Quantifiers

Publikation: AndetUndervisningsmateriale

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.
OriginalsprogEngelsk
Publikationsdato2016
Antal sider9
StatusUdgivet - 2016

Citationsformater