Exercise index of this lecture   Alphabetic index   Course home   

Exercises and solutions
Designkontrakter og ansvarsfordeling

9.1   Pre- og postbetingelser i CircularList  

På den tilknyttede slide er der vist pre- og postbetingelser for klassen CircularList. I betingelserne anvendes funktionerne empty(), countElements(), isCircular(), isFirst(Object), isLast(Object), retrieveSecond() og retrieveButLast().

Denne opgave går ud på at implementere ovennævnte funktioner som private operationer i klassen CircularList. Simuler pre- og postbetingelserne ved at kalde funktionerne hhv. først og sidst i klassen's metoder. Hvis der brydes en prebetingelse skal man udføre:

   throw new PreconditionBroken()

Tilsvarende skal et brud af en postbetingelse føre til udførelse af:

   throw new PostconditionBroken()

Download filen med min løsning af opgaven om Cirkulære lister. Denne fil indeholder endvidere de nødvendige erklæringer af de ovenfor nævnte exception klasser.

Udtrykkene i 'old ...' kan volde særlige problemer. Ideen med old er at kunne evaluere et udtryk i den programtilstand som bestod netop inden metoden blev kaldt. Derfor vil det være en mulighed at forudberegne disse 'old udtryk' i starten af metoden.

Solution
Herefter følger min løsning: 

class CircularList {
  
  private int length;
  private Linkable last;

  /** return the first Linkable objekt in the circular list */
  private Linkable firstLinkable(){
   if (length != 0)
    return(last.next());
   else return(null);  //does not make sense
  }

  /** return the Linkable objekt just before last */
  private Linkable butLastLinkable(){
   if (length == 0)
     return(null);
   else {
     Linkable link = last;
     while (link.next() != last) link = link.next();
     return (link);
   }
  }

  /** arrange that I become empty */
  private void emptyMe(){
    length = 0;
    last = null;
  }

  /** Arrange that I am a circular list with el as the only element */
  private void makeMeSingular(Object el){
    last = new Linkable(el);
    last.setNext(last);    
    length = 1;
  }

  /** Construct an empty circular list */
  public CircularList(){
    this.emptyMe();

    // post condition:
    if (!empty()) throw new PostconditionBroken();
  }

  /** Return my number of elements */
  public int size(){
    int res = length;

    // post condition
    if (!(res == countElements())) throw new PostconditionBroken();
    return(res);
  }

  /** Insert el as a new first element */
  public void insertFirst(Object el){
    // precondition
    if (full()) throw new PreconditionBroken();

    Linkable newLink;
    if (length == 0) {
      makeMeSingular(el);
    }
    else {
      newLink = new Linkable(el,firstLinkable());
      last.setNext(newLink);
      length = length + 1;
    }
    // postcondition:
    if (!(!empty() && isCircular() && isFirst(el))) 
      throw new PostconditionBroken();


  }
     
  /** Insert el as a new last element */
  public void insertLast(Object el){
    // precondition
    if (full()) throw new PreconditionBroken();

    Linkable newLink;
    if (length == 0) {
      makeMeSingular(el);
    }
    else{
      Linkable rememberOldLast = last;
      newLink = new Linkable(el,firstLinkable());
      last = newLink;
      rememberOldLast.setNext(last);
      length = length + 1;
    }

    // postcondition:
    if (!(!empty() && isCircular() && isLast(el))) 
      throw new PostconditionBroken();
  }

  /** Delete my first element */
  public void deleteFirst(){
    // precondition
    if (empty()) throw new PreconditionBroken();

    Object oldSecond = retrieveSecond();

    if (length <= 1)
      this.emptyMe();
    else{
      last.setNext(firstLinkable().next());
      length = length - 1;
   }

    // postcondition:
    if (!(empty() || (isCircular() && isFirst(oldSecond))))
      throw new PostconditionBroken();
  }

  /** Delete my last element */
  public void deleteLast(){
    // precondition
    if (empty()) throw new PreconditionBroken();

    Object oldButLast = retrieveButLast();

    if (length <= 1)
       this.emptyMe();
    else {
      Linkable theFirst = firstLinkable();
      last = butLastLinkable();
      last.setNext(theFirst);
      length = length - 1;
    }
    // postcondition:
    if (!(empty() || (isCircular() && isLast(oldButLast))))
      throw new PostconditionBroken();

  }

  /** Return my first element if any. Else return null */
  Object retrieveFirst(){
    // precondition
    if (empty()) throw new PreconditionBroken();

    Object res;
    if (length >= 0)
       res = last.next().data();
    else res = null;

    // postcondition
    if (!isFirst(res)) throw new PostconditionBroken();
    return res;
  }

  /** Return my last element if any. Else return null */
  Object retrieveLast(){
    // precondition
    if (empty()) throw new PreconditionBroken();

    Object res; 
    if (length >= 0)
       res = last.data();
    else res = null;

    // postcondition
    if (!isLast(res)) throw new PostconditionBroken();
    return res;
  }

  /** Return my string representation */
  public String toString(){
    StringBuffer str = new StringBuffer();
    if (length == 0)
      return("Empty circular list");
    else {
      Linkable link = firstLinkable();
      for (int i = 1; i <= length; i++){
        str.append(link.data().toString() + ",");
        link = link.next();
      }
      return (str.toString());
    }
  }

  private boolean empty(){
    return last==null;
  }

  private int countElements(){
    if (empty())
      return 0;
    else {
      Linkable ptr = last.next(); 
      int count = 1;
      while (ptr != last){
        count = count + 1;
        ptr = ptr.next();
      }
      return count;
    }
  }

  // kommer vi tilbage til last hvis vi følger next kæden length gange.
  private boolean isCircular(){
    Linkable ptr = last.next(); 
    for(int i = 1; i < length; i++) ptr = ptr.next();
    return ptr==last;
  }

  private boolean full(){
    return false;
  }

  private boolean isFirst(Object el){
    if (empty())
      return false;
    else return el == last.next().data();
  }

  private boolean isLast(Object el){
    if (empty())
      return false;
    else return el == last.data();
  }

  private Object retrieveSecond(){
   if (length < 2)
      throw new RuntimeException("It does not make sense to retrieve second element here");
      return last.next().next().data();
  }

  private Object retrieveButLast(){
    if (length < 2)
      throw new RuntimeException("It does not make sense to retrieve but last element here");
      return butLastLinkable().data();
  }
}


class Linkable {
  private Object data;
  private Linkable next;

  /** Return a Linkable object with null references in both data and next */ 
  Linkable(){
    data = null;
    next = null;
  }

  /** Return a Linkable object with null references in next, and the parameter as data */   
  Linkable(Object data){
    this.data = data;
    this.next = null;
  }

  /** Return a Linkable object with first parameter as data and second parameter as next */
  Linkable(Object data, Linkable next){
    this.data = data;
    this.next = next;
  }

  /** Return the data of this Linkable object */
  Object data(){
    return (data);
  }

  /** Return the reference to the next Linkable */
  Linkable next(){
    return (next);
  }

  /** Set the data field of this Linkable object */
  void setData(Object data){
    this.data = data;
  }

  /** Set the next field of this Linkable object */
  void setNext(Linkable next){
    this.next = next;
  }

} // Linkable


class AssertionBroken extends RuntimeException {
  public AssertionBroken(){
    super();
  }
}

class PreconditionBroken extends AssertionBroken {
  public PreconditionBroken(){
    super();
  }
}

class PostconditionBroken extends AssertionBroken {
  public PostconditionBroken(){
    super();
  }
}


 class CircListAppl{

  public static void main (String[] args){
    CircularList cl = new CircularList();

    cl.insertFirst(new Integer(1));
    cl.insertFirst(new Integer(2));
    cl.insertLast(new Integer(3));
    cl.insertLast(new Integer(4));

    System.out.println(cl);
    System.out.println(cl.size());

    cl.deleteFirst();
    cl.deleteLast();  
    cl.deleteFirst();

    System.out.println("size:" + cl);

    System.out.println(cl.retrieveLast());
    System.out.println(cl.retrieveFirst());

  }

}

Her er endvidere et link til det rene Java program .

9.2   Kontrakter i Bankkonto  

Denne opgave handler igen om én af vore favoriteksempler, nemlig klassen Konto. Ved øvelserne i lektion 3 blev der stillet en opgave om at repræsentere en Konto med en transaktionshistorie. Brug løsningen på den tidligere opgave hvis I har behov for at hente et passende udgangspunkt for denne opgave.

Forsyn klassen konto med en kontrakt. Mere specifikt:

    Lav pre- og postbetingelser på alle operationer i klassen Definer en klasseinvariant

Vær specielt opmærksom på invarianten, som skal sikre konsistens mellem datarepræsentationen (transaktionshistorien) og de eksterne egenskaber af kontoen.

(Man kan iøvrigt hente meget konkret inspiration til denne opgave i artiklen 'Applying Design by Contract').

9.3   Klasseinvariant i DoubleLinkable  

Vi har i en tidligere lektion studeret dobbeltkædede lister. Se her for den relevante slide.

Formuler en passende klasseinvariant for en dobbeltkædet liste, som udtrykker at dobbeltkædningen er i orden.

Skitser et prædikat (boolsk funktion) på klassen DoubleLinkable, som udtrykker at et enkelt led i kæden er 'i orden'.

Solution
Invarianten for en dobbeltkædet lister er: 

For alle indre kædeobjekter k skal der gælde 
   k.isPartOfDoubleLinking();
For et evt. første kædeobjekt k skal der gælde:
   k.isFirstOfDoubleLinking();
For et evt. sidste kædeobjekt k skal der gælde:
   k.isLastOfDoubleLinking();

Metoden isPartOfDoubleLinking(k) udtrykker uformelt at:

  k.next().previous() = k

og

  k.previous().next() = k

De to andre predikater er blot rand- og specialtilfælde af ovenstående.

Generated: Monday March 31, 2008, 12:09:02
on the system cs-unix