File Source: messagetype.java

         /* 
    P/P   *  Method: MessageType valueOf(String)
          * 
          *  Postconditions:
          *    init'ed(return_value)
          */
     1  package net.sourceforge.pebble.domain;
     2  
     3  /**
     4   * Represents a message type.
     5   *
     6   * @author    Simon Brown
     7   */
     8  public enum MessageType {
     9  
           /* 
    P/P     *  Method: net.sourceforge.pebble.domain.MessageType__static_init
            * 
            *  Postconditions:
            *    ENUM$VALUES == &new MessageType[](MessageType__static_init#4)
            *    ERROR == &new MessageType(MessageType__static_init#3)
            *    ENUM$VALUES[2] == &new MessageType(MessageType__static_init#3)
            *    INFO == &new MessageType(MessageType__static_init#1)
            *    ENUM$VALUES[0] == &new MessageType(MessageType__static_init#1)
            *    WARN == &new MessageType(MessageType__static_init#2)
            *    ENUM$VALUES[1] == &new MessageType(MessageType__static_init#2)
            *    new MessageType(MessageType__static_init#1) num objects == 1
            *    new MessageType(MessageType__static_init#2) num objects == 1
            *    new MessageType(MessageType__static_init#3) num objects == 1
            *    ...
            */
    10    INFO("info", "Info"),
    11    WARN("warning", "Warning"),
    12    ERROR("error", "Error");
    13  
    14    private String id;
    15    private String name;
    16  
           /* 
    P/P     *  Method: void net.sourceforge.pebble.domain.MessageType(String, int, String, String)
            * 
            *  Postconditions:
            *    this.id == id
            *    init'ed(this.id)
            *    this.name == name
            *    init'ed(this.name)
            */
    17    MessageType(String id, String name) {
    18      this.id = id;
    19      this.name = name;
    20    }
    21  
    22    public String getId() {
             /* 
    P/P       *  Method: String getId()
              * 
              *  Preconditions:
              *    init'ed(this.id)
              * 
              *  Postconditions:
              *    return_value == this.id
              *    init'ed(return_value)
              */
    23      return id;
    24    }
    25  
    26    public String getName() {
             /* 
    P/P       *  Method: String getName()
              * 
              *  Preconditions:
              *    init'ed(this.name)
              * 
              *  Postconditions:
              *    return_value == this.name
              *    init'ed(return_value)
              */
    27      return this.name;
    28    }
    29  
    30  }








SofCheck Inspector Build Version : 2.22510
messagetype.java 2010-Jun-25 19:40:32
messagetype.class 2010-Jul-19 20:23:40