Previous Contents

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.

• Time slots. The diary will consist of a number of time slots. We will not at this stage specify their length or structure.
• Activities. Each time slot can contain one activity. We will not at this stage specify the nature of activities. Note you might debate the idea that time slots can only contain one activity - much diary software does not enforce this condition. However, for the purposes of our illustrative example, we will require this.
• Calendar. The relationship between time slots and activities will be called a calendar. Given a time slot, the calendar will be able to tell us which, if any, activity is associated with that time slot.
• Not all time slots allowed. We will not permit all time slots to have an associated activity (in other words, not all time slots will be in the calendar). This is because we would like to have some concept of 'working hours'. Time slots that fall outside working hours will not be permitted to have an associated activity. (Again, we can question the realism of this requirement).
• Time slots unique and totally ordered. A time slot can only appear once in the calender, and furthermore time slots are totally ordered: that is, given any two time slots t and s, where t =/= s, then either t < s or s < t.

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.

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.

• Add. Add an entry in a slot if one is not present and the slot is in the calendar. Otherwise, return an error code.
• Delete. Delete the activity corresponding to a time slot if one is present and the slot is in the calendar. Otherwise, return an error code.
• Replace. Add an entry in a slot (overwriting any that is already present) provided the slot is in the calendar. Otherwise, return an error code.
• Lookup. Lookup the activity corresponding to a time slot (returning empty is there is none) provided the slot is in the calendar. Otherwise, return an error code.

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.

• Time slots. The first will define time slots. These will be pairs consisting of a Int representing an hour and a Day, where Day is a new sort. Note that this is a bit limited - we have no concept of a multi-week diary, and all time slots must be one hour long.
• Activities. The module defining activites will simply define a set of constants representing some plausibly-named 'activities' that you might reasonably expect to happen at work. We could have defined a much more complex, structured, notion of an activity. However, the simple model is sufficient to get the diary to work.
• Setup. Finally, we will define a module to initialise a diary to be completely empty.

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.

• Including. Because we are in this module equationally defining operators that appeared first in CALENDAR, we are effectively changing things from that earlier module. Hence we must use including instead of protecting.
• Day sort and constants. We introduce a new sort Day, and seven constants for the days of the week.
• Comparison operator for days. We already have a comparison operator for TimeSlot (in the first module CALENDAR) which we will equationally define in this new module. However, to do that, we will need an auxilliary operator to compare days.
• Comparing Time Slots. We equationally define the less-than operator for time slots. One time slot is less than another if either (a) its day is less, or (b) its day is the same but its hour is less.
• Comparing Days. We then define the less-than operator for days. This looks as if it could take lots of equations, but we can do most of it recursively and only need seven.
• Allowed Time Slots. Finally, using a membership axiom, we define those time slots we are prepared to allow into the calendar: these are, 9-5, monday-friday.

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