Aims

Recursive structures are common in many applications, notably in computer language processing. They present particular modelling challenges and so we devote a chapter to them. The aim here is to show how recursive data structures such as trees and graphs are defined and used through recursive traversal. We do not introduce new VDM language concepts at this stage, but consolidate the reader's knowledge and experience by showing how VDM copes with this important class of system. We add further abstraction lessons by considering the executability of functions.

Recursive data structures: trees

Recursion arises in many significant computing applications. In Chapter 7 we introduced recursive functions as a means of traversing collections of values, and illustrated their use on sequences. However, recursion is also central to an understanding of other data structures, including trees and graphs, that arise in many significant computing applications. This chapter explores the modelling of such recursive structures further. We begin by examining tree structures and illustrate their use by examining abstract syntax trees – an application area that underpins many applications in design and programming support environments, including VDMTools. We go on to examine more general graph structures, using an application from machine code optimisation to illustrate recursive traversal. The abstraction lesson in this chapter concerns the costs and benefits of executable models.

We begin by considering a common data structure: a tree. A tree is a collection of points (termed nodes) connected to each other by links (termed arcs).