rolodex
Class Rolodex

java.lang.Object
  |
  +--java.util.Observable
        |
        +--mvp.Model
              |
              +--rolodex.Rolodex

All Implemented Interfaces:

java.io.Serializable

public class Rolodex

extends mvp.Model

implements java.io.Serializable

Class Rolodex is the model class for the basic rolodex object, including the operations to add, delete, change, and find rolodex entries.

See Also:

Serialized Form

Field Summary

protected AddInputErrors	aie Error messages for the Add function
protected ChangeInputErrors	cie Error messages for the Change function
protected CardList	cl Simple list rep'n of the card list
protected DeleteInputError	die Error message for the Delerte function

Fields inherited from class mvp.Model

view

Constructor Summary

Rolodex(mvp.View v)
Construct an initially empty rolodex.

Method Summary

void	add(Card c) Add the given card to this if a card of the same id is not already there and there is room for another card.
void	change(Id id, Card c) Change the card of the given id in this to the given new card.
void	delete(Id id) Delete the card of the given id from this.
java.lang.String	dump() Dump this to stdout by dumping each card, in List.iterator order.
protected Card	find(Id id) Find the card of the given id.
CardList	find(Name n) Find all of the cards of the given name in this.
java.util.Iterator	getIterator() Provide an abstract iterator that will enumerate the cards of this.
void	print() Print this to stdout.
protected AddInputErrors	validateAddInput(Card c) Validate the given card per the precondition of Add.

Methods inherited from class mvp.Model

exit, getView, setView

Methods inherited from class java.util.Observable

addObserver, clearChanged, countObservers, deleteObserver, deleteObservers, hasChanged, notifyObservers, notifyObservers, setChanged

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

cl

protected CardList cl

Simple list rep'n of the card list

aie

protected AddInputErrors aie

Error messages for the Add function

die

protected DeleteInputError die

Error message for the Delerte function

cie

protected ChangeInputErrors cie

Error messages for the Change function

Constructor Detail

Rolodex

public Rolodex(mvp.View v)

Construct an initially empty rolodex. Initialize the error objects for each function that throws an exception.

 post: (exists (CardList cl) (this'.cl == cl) and (cl.Len() == 0))
           and
       (exists (AddInputErrors aie) (this'.aie == aie));
           and
       (exists (DeleteInputError die) (this'.die == die));
           and
       (exists (ChangeInputErrors cie) (this'.cie == cie));
                                                                   

Method Detail

add

public void add(Card c)
         throws AddInputErrors

Add the given card to this if a card of the same id is not already there and there is room for another card.

 pre:
      // There is no card in the input this with the same id as the given
      // input card.
      not CardAlreadyThere(c)

          and

      // The values of the given card fields are valid.
      CardIsValid(c)

          and

      // There is room for another card.
      (cl.Len() < MAXCARDS)

 post:
      // If none of the preconditions is violated, then a normal
      // postcondition holds, else an exception is thrown.
      if (not addPrecondViolated(c)) (
          // A card is in the output this iff it is in the input this or
          // it's the new card to be added.
          forall (Card c') this'.In(c') iff (In(c') or (c' == c))

              and

          // The size of this is increased by 1.
          (cl'.Length() == cl.Length() + 1)

              and

		// This has changed (as an observable object).
		this'.hasChanged() == true;
      )
      else (
          // An AddInputException is thrown if any of the preconditions
          // is violated.  The value of the exception flag is set for
          // each violated precondition via the ValidataAddInput
          // function. 
          (throw == aie) and (aie == ValidateAddInput(c))

          and

                                                                   

AddInputErrors

delete

public void delete(Id id)
            throws DeleteInputError

Delete the card of the given id from this.

 pre:
      // There is a card of the given id in the input this.
      exists (Card c' | In(c')) c'.getId() == id;

 post:
      // If the precondition is not violated, then a normal postcondition
      // holds, else an exception is thrown.
      if (deletePrecondViolated(c)) then (
          // A card is in the output this iff it is in the input this and
          // its id is different than the given id.
          forall (Card c')
              this'.In(c') iff (In(c') and (c'.id != id));

              and

		// This has changed (as an observable object).
		this'.hasChanged() == true;
      )
      else
          // A DeleteInputException is thrown if the precondition is
          // violated.
          throw == die;
                                                                   

DeleteInputError

change

public void change(Id id,
                   Card c)
            throws AddInputErrors,
                   ChangeInputErrors,
                   DeleteInputError

Change the card of the given id in this to the given new card.

 pre:
      // There is a card of the given id in the input this and that card
      // is not identical with the given input card, and the given card
      // is valid.
      exists (Card c' | In(c') (c'.getId() == id) and
          (c' != c) and CardIsValid(c);

 post:
      // If the precondition is not violated, then a normal postcondition
      // holds, else an exception is thrown.
      if (changePrecondViolated(c)) then (
          // A card is in the output this iff it is in the input this and
          // is not the card with the given id in the input this, or it's
          // the given input card.
          forall (Card c')
              this'.In(c') iff (In(c') and
                  (not exists (Card c'' | In(c''))
                      (c''.getId() == id) and (c'' == c')) or
                  (c' == c))

              and

		// This has changed (as an observable object).
		this'.hasChanged() == true;
      )
      else
          // A ChangeInputException is thrown if the precondition is
          // violated.
          throw == cie;
                                                                   

AddInputErrors

ChangeInputErrors

DeleteInputError

find

public CardList find(Name n)

Find all of the cards of the given name in this.

 post:
      // Cards in the output list consist of those in the input this with
      // the given name.
      forall (Card c)
           (cl.In(c) iff (In(c) and (c.getName() == n))

          and

      // The output card list is sorted by ascending order of card id.
      forall (int i, int j |
          (i >= 1) and (i <= cl.Length()) and
                  (j >= 1) and (j <= cl.Length()))
              if i < j then
                  cl.get(i).getId() < cl.get(j).getId();
                                                                   

getIterator

public java.util.Iterator getIterator()

Provide an abstract iterator that will enumerate the cards of this.

print

public void print()

Print this to stdout. In the current design, the specs are the same as dump below, q.v. In general, if there is a distinction between print and dump it is that the former produces a more nicely formated output than the latter, and printing may be in some sorted order whereas dumping will be in what ever the most convenient internal order is.

dump

public java.lang.String dump()

Dump this to stdout by dumping each card, in List.iterator order. Return just the string "Cards dumped to stdout."

Overrides:

dump in class mvp.Model

find

protected Card find(Id id)

Find the card of the given id. Return null of no such card is in this.

validateAddInput

protected AddInputErrors validateAddInput(Card c)

Validate the given card per the precondition of Add. Return the appropriately set AddInputErrors value. See the definition of AddInputErrors for further information.