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 |