UQ Students should read the Disclaimer & Warning

Note: This page dates from 2005, and is kept for historical purposes.

COMP3601 – Software Specification – Assignment Two (Hire Machine)

Specification (PDF, 123 KB)

I achieved 16 out of a possible 20 marks.

My Solution (PDF, 42 KB)

Source used to generate the pretty-printed solution above, is shown below.

Hire.mch
/*" {\bf COMP3601 - Assignment 2} {\bf Name: Ned Martin} {\bf Student Number: 40529927} % Defined for comments \newcommand{\com}{\vspace{-2.5ex}\em\tiny} \newcommand{\comb}{\vspace{-2.5ex}\hspace{6ex}\em\tiny} \newcommand{\ecom}{\normalsize\vspace{-2ex}} "*/ MACHINE Hire SETS ITEMS ; CUSTOMERS CONSTANTS maxitems, bag_total, total_items, number_of_item, bag_union PROPERTIES maxitems : NAT & bag_total : (ITEMS +-> NAT1) --> NAT1 & !bb . (bb : (ITEMS +-> NAT1) => bag_total(bb) = SIGMA(zz).(zz : dom(bb) | bb(zz))) & /*"\com total number of items hired to a customer \ecom"*/ total_items : (((CUSTOMERS * NAT) +-> (ITEMS +-> NAT1)) * CUSTOMERS) --> NAT & !(hh, cc) . ( hh : (CUSTOMERS * NAT) +-> (ITEMS +-> NAT1) & cc : CUSTOMERS => total_items(hh, cc) = SIGMA(zz) . (zz : ({cc} <| dom(hh)) | bag_total(({zz} <| hh)(zz))) ) & /*"\com total number of specific items on hire \ecom"*/ number_of_item : (((CUSTOMERS * NAT) +-> (ITEMS +-> NAT1)) * ITEMS) --> NAT1 & !(hh, ii) . ( hh : (CUSTOMERS * NAT) +-> (ITEMS +-> NAT1) & ii : ITEMS => number_of_item(hh, ii) = SIGMA(zz) . (zz : dom(hh) | bag_total(hh(zz))) ) & /*"\com merges two bags \ecom"*/ bag_union : ((ITEMS +-> NAT1) * (ITEMS +-> NAT1)) --> (ITEMS +-> NAT1) & !(ba, bb) . ( ba : ITEMS +-> NAT1 & bb : ITEMS +-> NAT1 => bag_union(ba |-> bb) = {xx, yy | xx : (dom(ba) \/ dom(bb)) & yy : NAT1 & yy = bag_total({xx} <| (ba \/ bb))} ) VARIABLES today, stock, hasHired INVARIANT today : NAT & stock : ITEMS +-> NAT & hasHired : (CUSTOMERS * NAT) +-> (dom(stock) +-> NAT1) & /*"\com customer cannot hire more than maxitems total \ecom"*/ !cc . (cc : CUSTOMERS => total_items(hasHired, cc) <= maxitems) & /*"\com cannot hire more items than those in stock \ecom"*/ !ii . (ii : dom(stock) => number_of_item(hasHired, ii) < stock(ii)) INITIALISATION today, stock, hasHired := 0, {}, {} OPERATIONS /*"Hire given instances of given item to given customer if items are available and customer has not already hired maxitems"*/ hire(item, customer, quantity, duration) = PRE /*"\comb item is valid stock \ecom"*/ item: dom(stock) & /*"\comb customer is a customer \ecom"*/ customer: CUSTOMERS & /*"\comb quantity is greater than none \ecom"*/ quantity: NAT1 & /*"\comb stock is available, that is, quantity is less than or equal to stock on hand minus stock hired \ecom"*/ quantity <= (stock(item) - number_of_item(hasHired, item)) & /*"\comb customer cannot hire more than maxitems \ecom"*/ total_items(hasHired, customer) + quantity <= maxitems & duration: NAT THEN /*"\comb add items hired for this customer \ecom"*/ hasHired(customer |-> (today + duration)) := bag_union( ( { (customer |-> (today + duration) ) } <| hasHired ) ( customer |-> (today + duration) ), { (item |-> quantity) } ) END; /*" Output a subset of hasHired which are overdue items where return date is less than today"*/ oi <-- overdue = PRE /*"\comb nothing to check \ecom"*/ true THEN /*"\comb io equals all overdue items \ecom"*/ oi := (dom(hasHired) |> 1..(today-1)) <| hasHired END END
Portions of code © Copyright 2004 Ned Martin

04-Jun-2004