File Source: message.java

         /* 
    P/P   *  Method: net.sourceforge.pebble.domain.Message__static_init
          */
     1  /*
     2   * Copyright (c) 2003-2006, Simon Brown
     3   * All rights reserved.
     4   *
     5   * Redistribution and use in source and binary forms, with or without
     6   * modification, are permitted provided that the following conditions are met:
     7   *
     8   *   - Redistributions of source code must retain the above copyright
     9   *     notice, this list of conditions and the following disclaimer.
    10   *
    11   *   - Redistributions in binary form must reproduce the above copyright
    12   *     notice, this list of conditions and the following disclaimer in
    13   *     the documentation and/or other materials provided with the
    14   *     distribution.
    15   *
    16   *   - Neither the name of Pebble nor the names of its contributors may
    17   *     be used to endorse or promote products derived from this software
    18   *     without specific prior written permission.
    19   *
    20   * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
    21   * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
    22   * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
    23   * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
    24   * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
    25   * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
    26   * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
    27   * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
    28   * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
    29   * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
    30   * POSSIBILITY OF SUCH DAMAGE.
    31   */
    32  package net.sourceforge.pebble.domain;
    33  
    34  import net.sourceforge.pebble.util.SecurityUtils;
    35  
    36  import java.util.Date;
    37  
    38  /**
    39   * Represents a message, created by Pebble for the user.
    40   *
    41   * @author    Simon Brown
    42   */
    43  public class Message {
    44  
    45    private MessageType type;
    46    private Date date;
    47    private String text;
    48  
           /* 
    P/P     *  Method: void net.sourceforge.pebble.domain.Message(MessageType, String)
            * 
            *  Postconditions:
            *    this.date == &new Date(Message#1)
            *    init'ed(this.text)
            *    this.type == type
            *    init'ed(this.type)
            *    new Date(Message#1) num objects == 1
            */
    49    public Message(MessageType type, String text) {
    50      this.type = type;
    51      setText(text);
    52      this.date = new Date();
    53    }
    54  
    55    public Date getDate() {
             /* 
    P/P       *  Method: Date getDate()
              * 
              *  Preconditions:
              *    init'ed(this.date)
              * 
              *  Postconditions:
              *    return_value == this.date
              *    init'ed(return_value)
              */
    56      return date;
    57    }
    58  
    59    public String getText() {
             /* 
    P/P       *  Method: String getText()
              * 
              *  Preconditions:
              *    init'ed(this.text)
              * 
              *  Postconditions:
              *    return_value == this.text
              *    init'ed(return_value)
              */
    60      return text;
    61    }
    62  
    63    private void setText(String text) {
             /* 
    P/P       *  Method: void setText(String)
              * 
              *  Postconditions:
              *    init'ed(this.text)
              * 
              *  Test Vectors:
              *    net.sourceforge.pebble.util.SecurityUtils:getUsername(...)@64: Addr_Set{null}, Inverse{null}
              */
    64      String username = SecurityUtils.getUsername();
    65      if (username != null) {
    66        this.text = "[" + username + "] " + text;
    67      } else {
    68        this.text = text;
    69      }
    70    }
    71  
    72    public MessageType getType() {
             /* 
    P/P       *  Method: MessageType getType()
              * 
              *  Preconditions:
              *    init'ed(this.type)
              * 
              *  Postconditions:
              *    return_value == this.type
              *    init'ed(return_value)
              */
    73      return type;
    74    }
    75  
    76    public boolean equals(Object o) {
             /* 
    P/P       *  Method: bool equals(Object)
              * 
              *  Preconditions:
              *    (soft) init'ed(o.date)
              *    (soft) init'ed(o.text)
              *    (soft) this.date != null
              *    (soft) init'ed(this.text)
              * 
              *  Postconditions:
              *    init'ed(return_value)
              * 
              *  Test Vectors:
              *    o: Inverse{null}, Addr_Set{null}
              *    o.text: Addr_Set{null}, Inverse{null}
              *    this == o: {0}, {1}
              *    this.text: Inverse{null}, Addr_Set{null}
              *    java.util.Date:equals(...)@82: {1}, {0}
              */
    77      if (this == o) return true;
    78      if (o == null || getClass() != o.getClass()) return false;
    79  
    80      final Message message = (Message) o;
    81  
    82      if (!date.equals(message.date)) return false;
    83      if (text != null ? !text.equals(message.text) : message.text != null) return false;
    84  
    85      return true;
    86    }
    87  
    88    public int hashCode() {
    89      int result;
             /* 
    P/P       *  Method: int hashCode()
              * 
              *  Preconditions:
              *    this.date != null
              *    init'ed(this.text)
              * 
              *  Presumptions:
              *    java.util.Date:hashCode(...)@90 in -222_153_480..222_153_480
              *    java.util.Date:hashCode(...)@90*29 + java.lang.String:hashCode(...) in -231..232-1
              * 
              *  Postconditions:
              *    (soft) init'ed(return_value)
              */
    90      result = date.hashCode();
    91      result = 29 * result + (text != null ? text.hashCode() : 0);
    92      return result;
    93    }
    94  
    95  }








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