month.java

### File Source: month.java

             /*
        P/P   *  Method: net.sourceforge.pebble.domain.Month__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 java.text.SimpleDateFormat;
        35  import java.util.*;
        36
        37  /**
        38   * Represents a blog at a monthly level. This manages a collection of Day instances.
        39   *
        40   * @author    Simon Brown
        41   */
        42  public class Month extends TimePeriod implements Permalinkable {
        43
        44    /** the parent, Year instance */
        45    private Year year;
        46
        47    /** an integer representing the month that this Month is for */
        48    private int month;
        49
        50    /** the collection of Day instances that this blog is managing */
        51    private Day[] dailyBlogs;
        52
        53    /** the last day in this month */
        54    private int lastDayInMonth;
        55
        56    /**
        57     * Creates a new Month based upon the specified Year and month.
        58     *
        59     * @param year    the owning Year instance
        60     * @param month         the month as an int
        61     */
        62    Month(Year year, int month) {
                 /*
        P/P       *  Method: void net.sourceforge.pebble.domain.Month(Year, int)
                  *
                  *  Preconditions:
                  *    month >= -231+1
                  *    year != null
                  *    year.blog != null
                  *    init'ed(year.year)
                  *
                  *  Presumptions:
                  *    java.util.Calendar:getActualMaximum(...)@71 in 0..232-2
                  *    net.sourceforge.pebble.domain.Blog:getCalendar(...)@69 != null
                  *
                  *  Postconditions:
                  *    this.blog == year.blog
                  *    this.blog != null
                  *    this.dailyBlogs == &new Day[](Month#1)
                  *    init'ed(this.date)
                  *    (soft) this.lastDayInMonth in 0..232-2
                  *    this.dailyBlogs.length == this.lastDayInMonth
                  *    this.month == month
                  *    this.month >= -231+1
                  *    this.year == year
                  *    this.year != null
                  *    ...
                  */
        63      super(year.getBlog());
        64
        65      this.year = year;
        66      this.month = month;
        67      setDate(getCalendar().getTime());
        68
        69      Calendar cal = getBlog().getCalendar();
        70      cal.setTime(getDate());
        71      this.lastDayInMonth = cal.getActualMaximum(Calendar.DAY_OF_MONTH);
        72
        73      // and create all days
        74      dailyBlogs = new Day[lastDayInMonth];
        75      for (int day = 1; day <= lastDayInMonth; day++) {
        76        dailyBlogs[day-1] = new Day(this, day);
        77      }
        78    }
        79
        80    private Calendar getCalendar() {
        81      // set the date corresponding to the 1st of the month
        82      // (this is used in determining whether another Month is
        83      // before or after this one)
                 /*
        P/P       *  Method: Calendar getCalendar()
                  *
                  *  Preconditions:
                  *    this.blog != null
                  *    this.month >= -231+1
                  *    this.year != null
                  *    init'ed(this.year.year)
                  *
                  *  Presumptions:
                  *    net.sourceforge.pebble.domain.Blog:getCalendar(...)@84 != null
                  *
                  *  Postconditions:
                  *    (soft) return_value != null
                  */
        84      Calendar cal = getBlog().getCalendar();
        85      cal.set(Calendar.YEAR, year.getYear());
        86      cal.set(Calendar.MONTH, month - 1);
        87      cal.set(Calendar.DAY_OF_MONTH, 1);
        88      cal.set(Calendar.HOUR_OF_DAY, 0);
        89      cal.set(Calendar.MINUTE, 0);
        90      cal.set(Calendar.SECOND, 0);
        91      cal.set(Calendar.MILLISECOND, 0);
        92
        93      return cal;
        94    }
        95
        96    /**
        97     * Gets a reference to the parent Year instance.
        98     *
        99     * @return  a Year instance
       100     */
       101    public Year getYear() {
                 /*
        P/P       *  Method: Year getYear()
                  *
                  *  Preconditions:
                  *    init'ed(this.year)
                  *
                  *  Postconditions:
                  *    return_value == this.year
                  *    init'ed(return_value)
                  */
       102      return year;
       103    }
       104
       105    /**
       106     * Gets an integer representing the month that this monthly blog is for.
       107     *
       108     * @return  an int representing the month (i.e. 1 to 12)
       109     */
       110    public int getMonth() {
                 /*
        P/P       *  Method: int getMonth()
                  *
                  *  Preconditions:
                  *    init'ed(this.month)
                  *
                  *  Postconditions:
                  *    return_value == this.month
                  *    init'ed(return_value)
                  */
       111      return month;
       112    }
       113
       114    /**
       115     * Gets the permalink to display all entries for this Month.
       116     *
       117     * @return  an absolute URL
       118     */
       119    public String getPermalink() {
                 /*
        P/P       *  Method: String getPermalink()
                  *
                  *  Preconditions:
                  *    this.blog != null
                  *
                  *  Postconditions:
                  *    return_value != null
                  *
                  *  Preconditions:
                  *    this.blog.permalinkProvider != null
                  *    (soft) net/sourceforge/pebble/domain/BlogManager.instance != null
                  *    (soft) init'ed(net/sourceforge/pebble/domain/BlogManager.instance.multiBlog)
                  *    (soft) init'ed(this.blog.id)
                  *
                  *  Test Vectors:
                  *    java.lang.String:length(...)@121: {0}, {1..232-1}
                  *    getPermalink(...)@120: Addr_Set{null}, Inverse{null}
                  */
       120      String s = getBlog().getPermalinkProvider().getPermalink(this);
       121      if (s != null && s.length() > 0) {
       122        return getBlog().getUrl() + s.substring(1);
       123      } else {
       124        return "";
       125      }
       126    }
       127
       128    /**
       129     * Determines whether this monthly blog has entries.
       130     *
       131     * @return    true if this blog contains entries, false otherwise
       132     */
       133    public boolean hasBlogEntries() {
                 /*
        P/P       *  Method: bool hasBlogEntries()
                  *
                  *  Preconditions:
                  *    (soft) this.dailyBlogs != null
                  *    (soft) this.dailyBlogs.length >= 1
                  *    (soft) this.dailyBlogs[...] != null
                  *    (soft) this.dailyBlogs[...].publishedBlogEntries != null
                  *    (soft) this.lastDayInMonth <= 232-2
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
       134      for (int i = 1; i <= lastDayInMonth; i++) {
       135        if (getBlogForDay(i).hasBlogEntries()) {
       136          return true;
       137        }
       138      }
       139
       140      return false;
       141    }
       142
       143    /**
       144     * Gets all blog entries for this month.
       145     *
       146     * @return  a List of BlogEntry instances, reverse ordered by date
       147     */
       148    public List<String> getBlogEntries() {
                 /*
        P/P       *  Method: List getBlogEntries()
                  *
                  *  Preconditions:
                  *    this.dailyBlogs != null
                  *    this.dailyBlogs.length <= 232-1
                  *    this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *    (soft) init'ed(this.dailyBlogs[...].blogEntries)
                  *    (soft) init'ed(this.lastDayInMonth)
                  *
                  *  Postconditions:
                  *    return_value == &new ArrayList(getBlogEntries#1)
                  *    new ArrayList(getBlogEntries#1) num objects == 1
                  */
       149      Day days[] = getAllDays();
       150      List blogEntries = new ArrayList();
       151      for (Day day : days) {
       152        blogEntries.addAll(day.getBlogEntries());
       153      }
       154      return blogEntries;
       155    }
       156
       157    /**
       158     * Gets the number of blog entries for this month.
       159     *
       160     * @return  an int
       161     */
       162    public int getNumberOfBlogEntries() {
                 /*
        P/P       *  Method: int getNumberOfBlogEntries()
                  *
                  *  Preconditions:
                  *    this.dailyBlogs != null
                  *    this.dailyBlogs.length <= 232-1
                  *    this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *    (soft) this.dailyBlogs[...].publishedBlogEntries != null
                  *    (soft) init'ed(this.lastDayInMonth)
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
       163      int count = 0;
       164      Day days[] = getAllDays();
       165      for (Day day : days) {
       166        count += day.getNumberOfBlogEntries();
       167      }
       168
       169      return count;
       170    }
       171
       172    /**
       173     * Gets an array of all Days.
       174     *
       175     * @return  a Collection of Day instances for all those days
       176     *          that have entries (this can return an empty collection)
       177     */
       178    public Day[] getAllDays() {
                 /*
        P/P       *  Method: Day[] getAllDays()
                  *
                  *  Preconditions:
                  *    this.dailyBlogs != null
                  *    this.dailyBlogs.length <= 232-1
                  *    this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *    (soft) init'ed(this.lastDayInMonth)
                  *
                  *  Postconditions:
                  *    return_value == &new Day[](getAllDays#1)
                  *    new Day[](getAllDays#1) num objects == 1
                  *    return_value.length == this.dailyBlogs.length
                  *    return_value.length <= 232-1
                  *    possibly_updated(return_value[...])
                  *    this.lastDayInMonth - this.dailyBlogs.length in -231..232-1
                  */
       179      Day blogs[] = new Day[dailyBlogs.length];
       180      for (int day = 0; day < dailyBlogs.length; day++) {
       181        blogs[day] = getBlogForDay(day + 1);
       182      }
       183
       184      return blogs;
       185    }
       186
       187    /**
       188     * Gets a Day instance for the specified day. This lazy loads Day
       189     * instances as needed.
       190     *
       191     * @param day   the day as an int (i.e. 1 to 31)
       192     * @return  the corresponding Day instance
       193     */
       194    public synchronized Day getBlogForDay(int day) {
       195      // some bounds checking
                 /*
        P/P       *  Method: Day getBlogForDay(int)
                  *
                  *  Preconditions:
                  *    day >= 1
                  *    this.dailyBlogs != null
                  *    this.dailyBlogs.length >= 1
                  *    day <= this.dailyBlogs.length
                  *    this.lastDayInMonth >= 1
                  *    this.lastDayInMonth - day in 0..232-2
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *
                  *  Postconditions:
                  *    return_value == this.dailyBlogs[...]
                  *    init'ed(return_value)
                  */
       196      if (day < 1 || day > lastDayInMonth) {
       197        throw new IllegalArgumentException("Invalid day of " + day + " specified, should be between 1 and " + lastDayInMonth);
       198      }
       199
       200      return dailyBlogs[day-1];
       201    }
       202
       203    /**
       204     * Gets a Day instance for the first day of the month.
       205     *
       206     * @return  the Day instance representing the first day in the month
       207     */
       208    public Day getBlogForFirstDay() {
                 /*
        P/P       *  Method: Day getBlogForFirstDay()
                  *
                  *  Preconditions:
                  *    this.dailyBlogs != null
                  *    this.dailyBlogs.length >= 1
                  *    this.lastDayInMonth >= 1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *
                  *  Postconditions:
                  *    return_value == this.dailyBlogs[...]
                  *    init'ed(return_value)
                  */
       209      return getBlogForDay(1);
       210    }
       211
       212    /**
       213     * Gets a Day instance for the last day of the month.
       214     *
       215     * @return  the Day instance representing the last day in the month
       216     */
       217    public Day getBlogForLastDay() {
                 /*
        P/P       *  Method: Day getBlogForLastDay()
                  *
                  *  Preconditions:
                  *    this.dailyBlogs != null
                  *    this.dailyBlogs.length >= 1
                  *    this.lastDayInMonth <= this.dailyBlogs.length
                  *    this.lastDayInMonth >= 1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *
                  *  Postconditions:
                  *    return_value == this.dailyBlogs[...]
                  *    init'ed(return_value)
                  */
       218      return getBlogForDay(lastDayInMonth);
       219    }
       220
       221    /**
       222     * Gets the last day of the month.
       223     *
       224     * @return  an int representing the last day in the month
       225     */
       226    public int getLastDayInMonth() {
                 /*
        P/P       *  Method: int getLastDayInMonth()
                  *
                  *  Preconditions:
                  *    init'ed(this.lastDayInMonth)
                  *
                  *  Postconditions:
                  *    return_value == this.lastDayInMonth
                  *    init'ed(return_value)
                  */
       227      return lastDayInMonth;
       228    }
       229
       230    /**
       231     * Gets the Month instance for the previous month.
       232     *
       233     * @return    a Month instance
       234     */
       235    public Month getPreviousMonth() {
                 /*
        P/P       *  Method: Month getPreviousMonth()
                  *
                  *  Preconditions:
                  *    this.month <= 13
                  *    this.year != null
                  *    (soft) this.month <= this.year.months.length + 1
                  *    (soft) this.year.blog != null
                  *    (soft) this.year.months != null
                  *    (soft) init'ed(this.year.months[...])
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  *
                  *  Preconditions:
                  *    (soft) this.year.blog.years != null
                  *    (soft) this.year.year >= -231+1
                  *
                  *  Postconditions:
                  *    init'ed(new ArrayList(Day#1) num objects)
                  *    init'ed(new ArrayList(Day#2) num objects)
                  *    init'ed(new ArrayList(Day#3) num objects)
                  *    init'ed(new Day(Month#2) num objects)
                  *    init'ed(new Day(Month#2).blog)
                  *    init'ed(new Day(Month#2).blogEntries)
                  *    init'ed(new Day(Month#2).date)
                  *    init'ed(new Day(Month#2).day)
                  *    init'ed(new Day(Month#2).month)
                  *    init'ed(new Day(Month#2).publishedBlogEntries)
                  *    ...
                  */
       236      return year.getBlogForPreviousMonth(this);
       237    }
       238
       239    /**
       240     * Gets the Month instance for the next month.
       241     *
       242     * @return    a Month instance
       243     */
       244    public Month getNextMonth() {
                 /*
        P/P       *  Method: Month getNextMonth()
                  *
                  *  Preconditions:
                  *    this.month >= 0
                  *    this.year != null
                  *    (soft) this.month - this.year.months.length in {-Inf..-1, 12..232-1}
                  *    (soft) this.year.blog != null
                  *    (soft) this.year.months != null
                  *    (soft) init'ed(this.year.months[...])
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  *
                  *  Preconditions:
                  *    (soft) this.year.blog.years != null
                  *    (soft) this.year.year <= 232-2
                  *
                  *  Postconditions:
                  *    init'ed(new ArrayList(Day#1) num objects)
                  *    init'ed(new ArrayList(Day#2) num objects)
                  *    init'ed(new ArrayList(Day#3) num objects)
                  *    init'ed(new Day(Month#2) num objects)
                  *    init'ed(new Day(Month#2).blog)
                  *    init'ed(new Day(Month#2).blogEntries)
                  *    init'ed(new Day(Month#2).date)
                  *    init'ed(new Day(Month#2).day)
                  *    init'ed(new Day(Month#2).month)
                  *    init'ed(new Day(Month#2).publishedBlogEntries)
                  *    ...
                  */
       245      return year.getBlogForNextMonth(this);
       246    }
       247
       248    /**
       249     * Determines if the this Month is before (in the calendar) the
       250     * specified Month.
       251     *
       252     * @return  true if this instance represents an earlier month than the
       253     *          specified Month instance, false otherwise
       254     */
       255    public boolean before(Month month) {
                 /*
        P/P       *  Method: bool before(Month)
                  *
                  *  Preconditions:
                  *    month != null
                  *    init'ed(month.date)
                  *    this.date != null
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
       256      return getDate().before(month.getDate());
       257    }
       258
       259    /**
       260     * Determines if the this Month is after (in the calendar) the
       261     * specified Month.
       262     *
       263     * @return  true if this instance represents a later month than the
       264     *          specified Month instance, false otherwise
       265     */
       266    public boolean after(Month month) {
                 /*
        P/P       *  Method: bool after(Month)
                  *
                  *  Preconditions:
                  *    month != null
                  *    init'ed(month.date)
                  *    this.date != null
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
       267      return getDate().after(month.getDate());
       268    }
       269
       270    /**
       271     * Given a Day, this method returns the Day instance for the
       272     * previous day.
       273     *
       274     * @param day   a Day instance
       275     * @return  a Day instance representing the previous day
       276     */
       277    Day getBlogForPreviousDay(Day day) {
                 /*
        P/P       *  Method: Day getBlogForPreviousDay(Day)
                  *
                  *  Preconditions:
                  *    day != null
                  *    init'ed(day.day)
                  *    (soft) day.day <= this.dailyBlogs.length + 1
                  *    (soft) this.dailyBlogs != null
                  *    (soft) this.dailyBlogs.length >= 1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *    (soft) init'ed(this.lastDayInMonth)
                  *    (soft) this.year != null
                  *    (soft) this.year.blog != null
                  *    (soft) this.year.months != null
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  *
                  *  Test Vectors:
                  *    day.day: {-231..1}, {2..232-1}
                  *
                  *  Preconditions:
                  *    (soft) this.month <= 13
                  *    (soft) this.month <= this.year.months.length + 1
                  *    (soft) this.year.blog.years != null
                  *    (soft) init'ed(this.year.months[...])
                  *    (soft) this.year.year >= -231+1
                  *
                  *  Presumptions:
                  *    getBlogForPreviousMonth(...).dailyBlogs.length@281 >= 1
                  *    getBlogForPreviousMonth(...).dailyBlogs@281 != null
                  *    getBlogForPreviousMonth(...).lastDayInMonth@281 >= 1
                  *
                  *  Postconditions:
                  *    init'ed(new ArrayList(Day#1) num objects)
                  *    init'ed(new ArrayList(Day#2) num objects)
                  *    init'ed(new ArrayList(Day#3) num objects)
                  *    init'ed(new Day(Month#2) num objects)
                  *    init'ed(new Day(Month#2).blog)
                  *    init'ed(new Day(Month#2).blogEntries)
                  *    init'ed(new Day(Month#2).date)
                  *    init'ed(new Day(Month#2).day)
                  *    init'ed(new Day(Month#2).month)
                  *    init'ed(new Day(Month#2).publishedBlogEntries)
                  *    ...
                  */
       278      if (day.getDay() > 1) {
    +  279        return this.getBlogForDay(day.getDay() - 1);
       280      } else {
    +  281        return year.getBlogForPreviousMonth(this).getBlogForLastDay();
       282      }
       283    }
       284
       285    /**
       286     * Given a Day, this method returns the Day instance for the
       287     * next day.
       288     *
       289     * @param day   a Day instance
       290     * @return  a Day instance representing the next day
       291     */
       292    Day getBlogForNextDay(Day day) {
                 /*
        P/P       *  Method: Day getBlogForNextDay(Day)
                  *
                  *  Preconditions:
                  *    day != null
                  *    init'ed(day.day)
                  *    day.day - this.lastDayInMonth in -232+1..6_442_450_943
                  *    init'ed(this.lastDayInMonth)
                  *    (soft) day.day < this.dailyBlogs.length
                  *    (soft) this.dailyBlogs != null
                  *    (soft) this.dailyBlogs.length >= 1
                  *    (soft) init'ed(this.dailyBlogs[...])
                  *    (soft) this.month - this.year.months.length in {-Inf..-1, 12..232-1}
                  *    (soft) this.year != null
                  *    ...
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  *
                  *  Test Vectors:
                  *    day.day - this.lastDayInMonth: {0..6_442_450_943}, {-232+1..-1}
                  *
                  *  Preconditions:
                  *    (soft) this.month >= 0
                  *    (soft) this.year.blog.years != null
                  *    (soft) init'ed(this.year.months[...])
                  *    (soft) this.year.year <= 232-2
                  *
                  *  Presumptions:
                  *    getBlogForNextMonth(...).dailyBlogs.length@296 >= 1
                  *    getBlogForNextMonth(...).dailyBlogs@296 != null
                  *    getBlogForNextMonth(...).lastDayInMonth@296 >= 1
                  *
                  *  Postconditions:
                  *    init'ed(new ArrayList(Day#1) num objects)
                  *    init'ed(new ArrayList(Day#2) num objects)
                  *    init'ed(new ArrayList(Day#3) num objects)
                  *    init'ed(new Day(Month#2) num objects)
                  *    init'ed(new Day(Month#2).blog)
                  *    init'ed(new Day(Month#2).blogEntries)
                  *    init'ed(new Day(Month#2).date)
                  *    init'ed(new Day(Month#2).day)
                  *    init'ed(new Day(Month#2).month)
                  *    init'ed(new Day(Month#2).publishedBlogEntries)
                  *    ...
                  */
       293      if (day.getDay() < lastDayInMonth) {
       294        return this.getBlogForDay(day.getDay() + 1);
       295      } else {
    +  296        return year.getBlogForNextMonth(this).getBlogForFirstDay();
       297      }
       298    }
       299
       300    /**
       301     * Gets a string representation of this object.
       302     *
       303     * @return  a String
       304     */
       305    public String toString() {
                 /*
        P/P       *  Method: String toString()
                  *
                  *  Preconditions:
                  *    init'ed(this.date)
                  *
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
       306      SimpleDateFormat sdf = new SimpleDateFormat("MMMM");
       307      return sdf.format(getDate());
       308    }
       309
       310  }

SofCheck Inspector Build Version : 2.22510

month.java | 2010-Jun-25 19:40:32
month.class | 2010-Jul-19 20:23:40