Previous Contents

A Diary Example in Maude

Chapter 15: A Diary Example in Maude

So far, the only sizeable examples we have seen have been hardware based. Hence in this (last) chapter, we will look at a Diary example in Maude, which is a reasonably large software specification example. As far as I am aware, the Diary example was first developed as an illustrative case study by IBM's Hursley Park Laboratories for a document describing the Z specification language. The complete Maude code can be found here.

15.1. The Abstract Diary

One of the keys to successful formal modelling of specifications in the initial stages is to ensure you think abstractly enough. In the case of diary software, it is easy to get bogged down in quite concrete details (how long are entries in the diary? what sort of things can go on? how is the software controlled and viewed?). Our initial diary will not concern itself with any of these things (and we will not consider some of them at all - even when we start to make the example more concrete). The key features are as follows.

Our first Maude module captures these requirements as far as is possible, without making time slots more concrete, as well as introducing some constants that are useful for status and error reporting.


fmod CALENDAR is

    *** Calendars are functions from
    *** timeslots to activities
    sorts TimeSlot? TimeSlot Activity Calendar .
    
    *** TimeSlot is a subsort of TimeSlot?
    *** and activities can
    *** only be associated with TimeSlot.
    
    subsort TimeSlot < TimeSlot? .

    *** Read a Calendar entry
    op _(_) : Calendar TimeSlot -> Activity .

    *** Write a Calendar entry
    op _(_/_) : Calendar TimeSlot Activity -> Calendar .

    *** Representation of an unused TimeSlot
    op empty : ->  Activity .


    *** The Calendar si *strictly* ordered
    op _<_ : TimeSlot? TimeSlot? -> Bool .

    *** Error codes that can be returned
    ops busy emptySlot : -> Calendar .

    vars s t : TimeSlot .
    var t' : TimeSlot? .
    var a : Activity .
    var c : Calendar .

    *** Define reading and writing - much like
    *** arrays and memory
    eq c(t / a)(t) = a .
    ceq c(t / a)(s) = c(s) if s =/= t .

    *** This must clearly be true.
    eq t' < t' = false .

endfm


This module defines four sorts TimeSlot, TimeSlot?, Activity and Calendar. TimeSlot? represents all possible times in the calendar; TimeSlot represents times when activities are allowed. Hence, TimeSlot is a subsort of TimeSlot?. Calendars will be functions from time slots to activities - appropriate read and write operators are declared and equationally defined (they are very similar to the earlier array example, and to the various microprocessor memories).

In addition, various constants are introduced. empty is used to represent an empty time slot; ; busy indicates an attempt to insert an ativity into a time slot that is already being used; and emptySlot represents an attempt to delete a non-existant activity. (Note there is no need to deal with attempts to add activities outside the legal time slots, because we will only define the relevant operators over TimeSlot: not TimeSlot?.) In addition we define a less-than operator on time slots (together with an obvious equation).

The next modules introduce various operators on the diary. We can obviously think of many, but we will restrict ourselves to the following.

15.1.1. Add an Entry

The module defining this operator is shown below.


fmod ADD-ENTRY is
    protecting CALENDAR .

    op addEntry : Calendar TimeSlot Activity ->
                 Calendar .

    var c : Calendar .
    var t : TimeSlot .
    var a : Activity .

    eq addEntry(c,t,a) =
        if (c(t) =/= empty) then
            busy
        else
            c(t / a)
        fi .
endfm


We just define a single operator addEntry that either updates the calendar, or returns an appropriate error code.

15.1.2. Delete an Entry

The module defining this operator is shown below.


fmod DEL-ENTRY is
    protecting CALENDAR .

    op delEntry : Calendar TimeSlot -> Calendar .

    var c : Calendar .
    var t : TimeSlot .

    eq delEntry(c,t) =
        if (c(t) == empty) then
            emptySlot
        else
            c(t / empty)
        fi .
endfm

Again, we just define a single operator delEntry that either updates the calendar, or returns an appropriate error code.

15.1.3. Replace an Entry

The module defining this operator is very similar to the two above.


fmod REPLACE-ENTRY is
    protecting CALENDAR .

    op replaceEntry : Calendar TimeSlot Activity ->
                     Calendar .

    var c : Calendar .
    var a : Activity .
    var t : TimeSlot .

    eq replaceEntry(c,t,a) = c(t / a) .
endfm

15.1.4. Lookup an Entry

The module defining this operator is shown below.


fmod LOOKUP is
    protecting CALENDAR .

    op lookup : Calendar TimeSlot -> Activity .

    var c : Calendar .
    var t : TimeSlot .

    eq lookup(c,t) = c(t) .

endfm

15.1.5. Bringing it Together

Finally, we define a module that collects these together - by simply importing them into a single module ABS-CALENDAR.


fmod ABS-CALENDAR is
    protecting CALENDAR .
    protecting ADD-ENTRY .
    protecting DEL-ENTRY .
    protecting REPLACE-ENTRY .
    protecting LOOKUP .
endfm

15.2. The Concrete Diary

Now, we will extend our abstract notion of a diary by saying precisely what time slots and activities are. Our definitions will be a bit basic - especially of activities - but they will allow us to do meaningful reductions. We will need three new modules.

15.2.1. Time Slots

We will use the built-in MachineInt sort to represent hours, and a new sort to represent days. It would have been better to also have a special Hour sort, but for simplicity we will not do so.


fmod TIME-SLOTS is
    protecting INT .

    *** We are going to modify CALENDAR, so including
    *** instead of protecting
    including ABS-CALENDAR .

    sorts Day .

    ops mon tue wed thur fri sat sun : -> Day .
    
    *** We divide the day into hours and days - hour:day
    op _:_ : Int Day -> TimeSlot? .
    
    *** (It's actually a bit tacky to just leave hours as
    *** integers, but simpler.)

    op _<_ : Day Day -> Bool .

    var i : Int .
    vars h h1 h2 : Int .
    vars d d1 d2 : Day .

    *** When is one TimeSlot less than another?
    eq (h1 : d1) < (h2 : d2) =
        if ((d1 < d2) or (d1 == d2) and (h1 < h2)) then
            true
        else
            false
        fi .

    *** A [slightly arbitrary] ordering on days
    eq sun < d = if (d =/= sun) then true else false fi .
    eq mon < d = if (d =/= mon) then sun < d
                 else false fi .
    eq tue < d = if (d =/= tue) then mon < d
                 else false fi .
    eq wed < d = if (d =/= wed) then tue < d
                 else false fi .
    eq thur < d = if (d =/= thur) then wed < d
                 else false fi .
    eq fri < d = if (d =/= fri) then thur < d
                 else false fi .
    eq sat < d = false .

    *** We are going to allow times
    *** from 9 : mon to 16 : fri
    *** in the diary
    cmb (h : d) : TimeSlot if
        (h > 8) and (h < 17) and
           (d =/= sat) and (d =/= sun) .
endfm

This is the longest and most complex module. The main issues are discussed below.

15.2.2. Activities

The next module just defines some basic, trivial 'activities' as constants.


fmod ACTIVITIES is
    protecting ABS-CALENDAR .

    ops staffMeeting interview bossVisiting
        leavingParty : -> Activity .
endfm

15.2.3. Concrete Calendar

Our final module brings together time slots and activities, and also defines an empty calendar.


fmod CONCRETE-CALENDAR is
    protecting TIME-SLOTS .
    protecting ACTIVITIES .
    
    op initCal : -> Calendar .

    var h : Int .
    var d : Day .
    
    eq initCal(h : d) = empty .
endfm

15.3. Sample Reduction

Here are two sample reductions. First, add a staff meeting in at 9.00 on tuesday, and then lookup the activity at 9.00 tuesday. It should be a staff meeting.


red lookup(addEntry(initCal,(9 : tue), staffMeeting),
(9 : tue)) .

We get:


reduce in CONCRETE-CALENDAR : lookup(addEntry(initCal, 9 : tue, staffMeeting),
    9 : tue) .
rewrites: 14 in 0ms cpu (0ms real) (~ rewrites/second)
result Activity: staffMeeting


If we do the same but this time lookup 9.00 on monday, we should get an empty slot.


red lookup(addEntry(initCal,(9 : tue), staffMeeting),
(9 : mon)) .

The result is:


reduce in CONCRETE-CALENDAR : lookup(addEntry(initCal, 9 : tue, staffMeeting),
    9 : mon) .
rewrites: 24 in 0ms cpu (0ms real) (~ rewrites/second)
result Activity: empty

Previous Contents