public class TimeOfDay {
 
    private int hour;
 
    private int minutes;
 
    private int seconds;
 
    public TimeOfDay(int hour, int minutes, int seconds) {                
        // Code Block : Precondition declaration
        // by default All method has a precondition, 
        // postoncistions with value equals true,
        pre { //lables are optionals
              valid_hour: hour >=0 && hour <=23;
              valid_minutes: minutes >=0 && minutes <=59;
              valid_seconds: seconds >=0 && seconds <=59; 
             }  
 
        this.hour = hour;
        this.minutes = minutes;
        this.seconds = seconds;
  
       // Code Block : Postcondition declaration
        post {
               hour == this.hour;
               minutes == this.minutes;
               seconds == this.seconds;
             }              
    }
 
    public TimeOfDay() {
    }
 
    public int getHour() {
        return hour;
    }
 
    public int getMinutes() {
        return minutes;
    }
 
    public int getSeconds() {
        return seconds;
    }
 
    public void setHour(int hour) {
        pre { hour >= 0 && hour <= 23 }
                            
          this.hour = hour;
          
       post { getMinutes() == old getMinutes()
             getSeconds() == oldgetSeconds() 
            } 
 
    }
    //Others Methods
    
    // Code Block: Invariant declarations
    invariant {getHour() >= 0 && getHour() <= 23;    
               getMinutes() >= 0 &&  getMinutes() <= 59;  
               getSeconds() >= 0 &&  getSeconds() <= 59;
              } 
}
 
   

interface Stringable<T> {

  public String toString();
  static public T valueOf(String s);

(or, even cooler, declare a constructor)
  public T(String s); 
}