UQ Students should read the Disclaimer & Warning
Note: This page dates from 2005, and is kept for historical purposes.
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>COMP3601 - Assignment 2 - Hire Machine</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<style type="text/css">
<!--
.wrong {
background: #FF9999;
}
body {
background: url(_img/DSC04989.jpg) fixed center;
font-family: "Arial Unicode MS", Arial, Helvetica, sans-serif;
}
th, td, textarea {
border: 1px solid #000000;
padding: 0 1ex;
background: transparent;
overflow: hidden;
}
table {
border: none;
}
-->
</style>
</head>
<body>
<h1>COMP3601 – Software Specification – Assignment Two (Hire Machine) </h1>
<p><a href=".//COMP3601-assignment-2-specification.pdf">Specification</a> (PDF, 123 KB) </p>
<p>I achieved 16 out of a possible 20 marks. </p>
<p><a href=".//COMP3601-assignment-2-Hire.mch.pdf">My Solution</a> (PDF, 42 KB) </p>
<p>Source used to generate the pretty-printed solution above, is shown below. </p>
<p>Hire.mch<br />
<textarea name="b" cols="82" rows="114" readonly="readonly" title="B Code">
/*"
{\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
</textarea>
<br />
Portions of code © Copyright 2004 Ned Martin</p>
<p>04-Jun-2004</p>
</body>
</html>