nedmartin - UNI - COMP3601 - Assignment 1

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 1 - Library 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 &ndash; Software Specification &ndash; Assignment One (Library Machine)</h1>

<p><a href=".//COMP3601-assignment-1-specification.pdf">Specification</a> (PDF, 105 KB)</p>

<p>I achieved 19 out of a possible 20 marks. </p>

<p><a href=".//COMP3601-assignment-1-ALibrary.mch.pdf">My Solution</a> (PDF,

    30 KB) </p>

<p>Source used to generate the pretty-printed solution above, is shown below. </p>

<p>ALibrary.mch<br /> 

    <textarea name="b" cols="82" rows="137" readonly="readonly" title="B Code">/*&quot;





{\bf COMP3601 - Assignment 1}



{\bf Name: Ned Martin}



{\bf Student Number: 40529927}





&quot;*/





MACHINE           Library



SETS

  BOOKID; BOOKDESC;

  READERID; READERDESC;

  LOANTYPE



CONSTANTS   maxloans



PROPERTIES  maxloans : NAT



VARIABLES

  books, readers, reserved, onLoanTo, today, loanTypeDuration,

  bookLoanType, returnDayOfBook



INVARIANT

  books : BOOKID +-> BOOKDESC &amp;

  readers : READERID +-> READERDESC &amp;

  reserved : POW BOOKID &amp;

  onLoanTo : BOOKID +-> READERID &amp;

  today : NAT &amp;

  loanTypeDuration : LOANTYPE --> NAT &amp;

  bookLoanType : BOOKID +-> LOANTYPE &amp;

  returnDayOfBook : BOOKID +-> NAT &amp;

  reserved &lt;: (dom(books) - dom(onLoanTo)) &amp;

  dom(onLoanTo) &lt;: dom(books) &amp;

  ran(onLoanTo) &lt;: dom(readers) &amp;

  ! rr . (rr : dom(readers) => (

       card(onLoanTo  |> {rr}) &lt;= maxloans)

       ) &amp;

  /* Only library books have a loan type */

  dom(bookLoanType) &lt;: dom(books) &amp;

  /* All borrowed books have a loan type */

  dom(onLoanTo) &lt;: dom(bookLoanType) &amp;

  /* No reserved book has a loan type */

  reserved /\ dom(bookLoanType) = {} &amp;

  /* A book is on loan if and only if it has a return date */

  dom(onLoanTo) = dom(returnDayOfBook)



INITIALISATION

  books, readers, reserved, onLoanTo, today, loanTypeDuration, bookLoanType, returnDayOfBook := (

    {},{},{},{},0,{xx, yy | xx : LOANTYPE &amp; yy : NAT},{},{}

    )



OPERATIONS



borrow_book(bookNo, readerNo) =

  PRE

    bookNo : dom(books) - (

     (reserved \/ dom(onLoanTo))

    ) &amp;

    readerNo : dom(readers) &amp;

    card(onLoanTo |> {readerNo}) &lt; maxloans &amp;

    /* Book has a loantype */

    bookNo : dom(bookLoanType)

  THEN

    onLoanTo := onLoanTo &lt;+ { bookNo |-> readerNo} ||

    /* Return date of book = bookNo |-> (N + today) where N = N from BOOKID |-> LOANTYPE |-> N */

    returnDayOfBook := returnDayOfBook &lt;+ {bookNo |-> ((bookLoanType ; loanTypeDuration)(bookNo) + today)}

  END;



remove_book(bookNo) =

  PRE

    bookNo : BOOKID &amp;

    bookNo : dom(books) &amp;

    bookNo /: dom(onLoanTo)

  THEN

    books := {bookNo} &lt;&lt;| books ||

    reserved := reserved - {bookNo} ||

    /* Remove book with bookNo from bookLoanType */

    bookLoanType := {bookNo} &lt;&lt;| bookLoanType

  END;



add_to_reserve(bookNo) =

  PRE

    bookNo : dom(books) - dom(onLoanTo) &amp;

    bookNo /: reserved

  THEN

    reserved := reserved \/ {bookNo} ||

    bookLoanType := {bookNo} &lt;&lt;| bookLoanType

  END;



new_day =

  PRE

    true

  THEN

    /* Increment today */

    today := today + 1

  END;



change_loan_type(bookNo, newLoanType) = 

  PRE

    bookNo : dom(books) &amp;

    bookNo /: reserved &amp;

    newLoanType : LOANTYPE

  THEN

    /* Insert/modify {bookNo |-> newLoanType} in bookLoanType */

    bookLoanType := bookLoanType &lt;+ {bookNo |-> newLoanType}

  END;



change_duration(loanType, newDuration) =

  PRE

    loanType : LOANTYPE &amp;

    newDuration : NAT

  THEN

    /* Insert/modify {loanType |-> newDuration} into loanTypeDuration */

    loanTypeDuration := loanTypeDuration &lt;+ {loanType |-> newDuration}

  END;



ob &lt;-- overdue_books =

  PRE

    true

  THEN

    /* Return ob where ob = {BOOKID |-> READERID} if returnDay(bookID) &lt; today and was onloan */

    ob := {xx | xx : dom(returnDayOfBook) &amp; returnDayOfBook(xx) &lt; today} &lt;| onLoanTo

  END



END

</textarea>

    <br />

    Portions of code &copy; Copyright 2004 Ned Martin</p> 

<p>04-Jun-2004</p> 

</body>

</html>
Menu Ned Martin’s Personal Nightmare — COMP3601 - Assignment 1 - Library Machine
