Formal Specification

Lecture 4

Composite Objects

Mohamed Mead
 Aims
Learning Outcomes At the end of this lecture you should
be able to:
 Identify when it is appropriate to use a composite object type

 Use the composite object operators (make, selection and mu)

 Add an invariant to a composite object type

 Use the composite object type to help model systems in VDM-SL

 Composite Types
 Use a VDM-SL composite object type when you need to
associate more than one type with an object

 For example, a time value consists of hours, minutes and

seconds types: types
Time :: hour: N
minute: N
second: N

 The Time type can be used to specify types of state variables. For
example, importantTimes is a set of Time objects:
importantTimes: Time-set
 Composite objects – general format
 The general format of a composite object comprises the object name
followed by the symbol :: followed by each fieldname and its type, the
field name and type separated by a colon (:)

types
TypeName :: fieldname1 : Type1
fieldname2 : Type2
…
 Composite objects - operations
VDM-SL supports three operations on composite object
types:
 make – to make composite objects

 selectors – to access specific fields of an object

 mu – to change the value of specific fields

.
 Composite objects – make function

 The most important composite object operator is the make function,

which creates a new object of a given composite object type. The general
format is:

 mk-CompositeObjectTypeName (parameter list)

 For example, we can make a Time object, named someTime, for the time
16 hours, 20 minutes and 44 seconds:

someTime = mk-Time ( 16 , 20 , 44 )
 Composite object invariants

 We can associate an invariant with the composite object type

 For example, not all combinations of hour/minute/time are valid:

 strangeTime = mk-Time (36, 20, 44)

 The invariant follows the type definition:

types
Time :: hour: N
minute: N
second: N
inv mk-Time (h, m, s) ∆ h < 24 ∧ m < 60 ∧ s < 60

7
 Composite objects – selectors

 We can refer to a field of a composite object by using a selector operator

 Individual fields are selected by the dot operator '.’ followed by the name of a field

 For example, if:

someTime = mk-Time ( 16 , 20 , 44 )

 then, someTime.minute is 20

 and, someTime.hour is 16

8
 Composite objects – mu function

 The mu function, represented by the symbol 𝛍𝛍, returns a new composite

object from another composite object, but with one or more fields
changed
 For example, we can use the mu function to change the hour of someTime to 15:

 newTime = 𝛍𝛍 (someTime, hour ↦ 15)

 More than one field may be changed in a mu function

 For example, we can set the minutes and seconds fields of someTime to zero:

 newTime = 𝛍𝛍 (someTime, minute ↦ 0, second ↦ 0)

9
 Case study

 The Disk Scanner Case Study

10
 The Disk Scanner

 Consider a piece of software designed to keep track of damaged blocks

on the surface of a disk.

 A disk is divided into a number of tracks and each track into a number of
sectors.

 A block is identified, therefore, by giving both a track number and a

sector number
 (i.e. block = <track#, sector#>)

11
 disk, tracks, sectors and blocks
disk

track

sector

block = <track#, sector#>

12
 The UML specification

DiskScanner Block
damagedBlocks: Block [*]
track: Integer
sector: Integer
addBlock(Integer, Integer)
removeBlock (Integer, Integer)
isDamaged(Integer, Integer): Boolean A block comprises a track
getBadSectors(Integer): Integer [*] and a sector number

13
 Specifying the data model in VDM-SL

Block
types track: Integer
Block :: track: N sector: Integer
sector: N

state DiskScanner of DiskScanner

damagedBlocks: Block-set
damageBlocks: Block [*]
init mk-DiskScanner (dB) ∆ dB = { }
end …

14
 The addBlock operation

addBlock (trackIn: N, sectorIn: N )

ext wr damagedBlocks: Block-set

pre mk-Block (trackIn, sectorIn) ∉

damagedBlocks

post damagedBlocks = damagedBlocks ∪

{ mk-Block (trackIn, sectorIn) }

15
 The removeBlock operation

removeBlock (trackIn: N, sectorIn: N )

ext wr damagedBlocks: Block-set

pre mk-Block (trackIn, sectorIn) ∈ damagedBlocks

post damagedBlocks = damagedBlocks \

{ mk-Block (trackIn, sectorIn) }

16
 The isDamaged operation

isDamaged (trackIn: N, sectorIn: N ) query : B

ext rd damagedBlocks: Block-set

pre TRUE

post query ⇔
mk-Block (trackIn, sectorIn) ∈ damagedBlocks

17
 The getBadSectors operation

getBadSectors (trackIn : N) list : N-set

ext rd damagedBlocks: Block-set

pre TRUE

post list =
{ b.sector | b ∈ damagedBlocks ● b.track = trackIn }

18
 The complete VDM-SL specification
types
Block :: track: N
sector: N
state DiskScanner of
damagedBlocks: Block-set
init mk-DiskScanner (dB) ∆ dB = { }
end
operations
addBlock (trackIn: N, sectorIn: N )
ext wr damagedBlocks: Block-set
pre mk-Block (trackIn, sectorIn) ∉ damagedBlocks
post damagedBlocks = damagedBlocks ∪ { mk-Block (trackIn, sectorIn) }
removeBlock (trackIn: N, sectorIn: N )
ext wr damagedBlocks: Block-set
pre mk-Block (trackIn, sectorIn) ∈ damagedBlocks
post damagedBlocks = damagedBlocks \ { mk-Block (trackIn, sectorIn) }
isDamaged (trackIn: N, sectorIn: N ) query : B
ext rd damagedBlocks: Block-set
pre TRUE
post query ⇔ mk-Block (trackIn, sectorIn) ∈ damagedBlocks
getBadSectors (trackIn : N) list : N-set
ext rd damagedBlocks: Block-set
pre TRUE
post list = { b.sector | b ∈ damagedBlocks ● b.track = trackIn }
19
 Case study

 The Process Management Case Study

20
 A process management system
In multi-tasking operating systems processes are identified by a unique process
identification number (pid).
When a process is created it joins the list of waiting processes, in the READY state.
(admit)
Processes are allocated to the CPU in a simple first-in-first-out policy:
• When the CPU becomes available, the first READY process in the queue is
allocated to the CPU and removed from the waiting list. (dispatch)
Each running process is allotted a fixed amount of CPU time (a quantum). If a
process uses up its allotted time before it terminates, it is placed back at the end
of the waiting queue with a READY status (timeout); if it has finished, it is removed
from the system (not put back in the queue). (terminate)
If the process did not time out but could not proceed for some reason (e.g. waiting
for an input/output operation), it is put back at the end of the waiting queue with
a BLOCKED status. (block)
When a blocked process is ready to be processed again, it is woken up from its
BLOCKED status and is once again in a READY state. (wakeup)
21
 process management – diagram

• Note that there is no reference in this diagrammatic model to the

waiting or running attributes,
• Reference is made only to states (new, ready, running terminated,
blocked), and to operations (admit, dispatch, terminate, timeout,
wakeup, block)
22
 The UML specification

ProcessManagement Process
running: String id: String
waiting: Process[*] status: Status
admit(String)
dispatch()
timeOut() <<enumeration>>
block() Status
wakeUp(String) READY
terminate() BLOCKED

23
 THANK YOU

24