Question 6

Consider the following scenario. -

A piece of software stores information about digital songs and keeps track of when they were listened to Each song is associated with a song name, an artist and an album title; each song is also associated with a unique identifier.

We assume the existence of a number of basic types.:

[SongName, Artist, Album Title, Id)

We also assume that a set, Time, has been defined. We algo assume an accompanying ordering relation, <_Time, and a special element miltirne C Time.

We also assunie an abbreviation, Length:

Length == N

Two structures are of interest to us. The first, songs, captures the details of the songs stored by our software; the second, plays, captures 'play details' - which songs were played and when:songs : Id -I-^, (SongNarne x Artist x Album Title x Length x Time) plays : seq (Id x Time)

Each element of the range of songs is a quintuple, consisting of: a song name; an artist; an album title; the length of the song (in terms of seconds); and the time at which the song was added.

Each element of plays is a pair, detailing which songs were played and when. So, for example, if the song associated with the identifier idl has been played three times, we would expect to see three entries for idl in plays_

The expectation is that each identifier appearing in plays will also appear in songs, that niltime will not appear in the range of plays, and that the elements of plays will be ordered from earliest to latest.

Add three constraints to the above axiomatic definition to enforce this behaviour.

Question 7

Building upon the definitions of Question 6, define set comprehensions that capture the following.

(a)   The set of all 'duplicate' songs - defined as (SongName, Artist) pairs - which appear in songs more than once.

(b)   The set of all songs___ again, defined as (SongName, Artist) pairs -
which have not been played.

(c)   The set of albums which have had none of their tracks played.

(d)   The set of all songs__ again, defined as (SongName, Artist) pairs -
which have been played more than 10 times.

Question 8

(a)   Define a recursive function, totalplaytirne, that sums up the length of time of the played songs appearing in a given sequence of type seq (Id x Time). Your function will need to make reference to songs.

(b)   Show, via an inductive proof, that

V s, t seq (Id x Time) •

totalplaytime (s t) = totalplaytime (s) totalplaytime (t)

Question 9

A structure combining information from songs and plays can be defined using the following definition:

SongsAndPlaysList == seq SongDetails 

We assume the existence of the following abbreviation:

SongDetails ==  Id × SongName × Artist × AlbumTitle ×  Length × Time × Time × N 

Here, the details of each song consists of: an identifier; a song name; an artist; an album title; the song length; the date it was added; the last time it was played; and the number of times it has been played.

(a) A valid element of SongsAndPlaysList will: ensure that there are no duplicate identifiers and ensure that any 'last played' time is later than

any 'date added' time. Define such a ValidSongsAndPlaysList structure. (b) Define a specific ValidSongsAndPlaysList, songs_and_plays, the values of which are defined by the values of songs and plays of Question 6.

(c) Show how the set comprehensions of Question 7 might be recast as set comprehensions on the sequence of part (b).

(d) Show how the recursive function of Question 8 might be recast as a function that takes a sequence of type seq SongDetails as input.

Question 10

You have been informed that the following statements are true:

• "If the team wins all of its league matches, then the team will win the league."

• "The team wins the cup if, and only if, the team wins all of its cup matches."

Assume that: AC represents "wins all cup matches"; AL represents "wins all league matches"; WC represents "wins the cup"; and WL represents "wins the league".

By using the above, prove each of the following via a proof tree.

(a) AC  Ù AL  => WC Ù WL  ( where AND = Ù)

(b) AC V AL => WC V WL (where V = or)

Each step in your tree should be labelled and justified by a basic introduction or elimination rule from our system.