[Prev][Next][Index]
Calendar traits
I think Jim's position is quite reasonable. So I'll offer below
my calendar traits for public consumption.
The traits are roughly in topological order below.
RawDates just defines the tuple of abstract values and the appropriate order.
It should be the most useful trait as it applies to many different calendars.
It turns out that there are many different calendars that have been
(historically) in use. The common Western calendar months are
in trait WesternMonths. I leave it to others to write up the Jewish, Islamic,
Chinese, etc. calendars. (I'm happy put them in a calendar Handbook if you
want to maintain what you contribute.)
In the Western calendar there are also variations. The basics are described
in the trait JulianGregorian. It depends on two dates (trait
GregorianAssumptions) telling when the switch was made from the
Julian to the Gregorian Calendar. Unfortunately, this
switch took place in different years in different countries.
(An additional complication is that different parts of the world are now in
different countries than they were...) If you are working in the US or
England, you can use the trait EnglishDate; this will also work if you
don't care about dates before (say) 1950. Traits CatholicDate and RussianDate
can be used for other countries. I leave it to others to make up traits
appropriate for other Western countries. If you're a historian, all of this
will probably be grossly inadequate.
Corrections and comments on either style or documentation are welcome.
Let's make this a test case for what should be included in offerings like this.
I think the author's name and a brief synopsis should be acceptable.
If we make our stylistic requirements too strict, then we may exclude
otherwise useful contributions. (I'm also *not* looking forward to endless
discussions about prettyprinting.) But at this stage perhaps some discussion
of LSL style is not out of bounds.
Once the bugs are worked out, I'll make them available by WWW;
does anyone have a program to turn ASCII LSL into HTML automatically?
(If so, it would be great to share *that*.)
Gary
P.S. If you want these in files, you'll have to split this up manually;
each file starts with a line of the form: % @(#)$Id ...
% @(#)$Id: RawDates.lsl,v 1.2 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: structure of dates
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
RawDates(D): trait
includes Integer, DerivedOrders(D) % from LSL Handbook of [Guttag-Horning93]
D tuple of year: Int, month: Int, day: Int
introduces
__<=__, __<__, __>=__, __>__: D, D -> Bool
asserts
\forall d1,d2: D
(d1 <= d2) == (d1.year < d2.year)
\/ ((d1.year = d2.year) /\ (d1.month < d2.month))
\/ ((d1.year = d2.year) /\ (d1.month = d2.month)
/\ (d1.day <= d2.day));
(d1 < d2) == (d1 <= d2 /\ not(d1 = d2));
(d1 > d2) == (d2 < d1)
% @(#)$Id: WesternMonth.lsl,v 1.2 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: dates and names of months as in the current Western calendar
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
WesternMonth(D): trait
includes RawDates(D)
introduces
January, February, March, April, May, June,
July, August, September, October, November, December: -> Int
days_in_month: Int, Int -> Int
asserts
\forall y: Int
January == 1; days_in_month(January, y) == 31;
February == 2; ~(mod(y,4) = 0) => (days_in_month(February, y) = 28);
28 <= days_in_month(February, y)
/\ days_in_month(February, y) <= 29;
March == 3; days_in_month(March, y) == 31;
April == 4; days_in_month(April, y) == 30;
May == 5; days_in_month(May, y) == 31;
June == 6; days_in_month(June, y) == 30;
July == 7; days_in_month(July, y) == 31;
August == 8; days_in_month(August, y) == 31;
September == 9; days_in_month(September, y) == 30;
October == 10; days_in_month(October, y) == 31;
November == 11; days_in_month(November, y) == 30;
December == 12; days_in_month(December, y) == 31;
% @(#)$Id: GregorianAssumptions.lsl,v 1.2 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: information about when the Gregorian calendar started
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
GregorianAssumptions(D): trait
includes RawDates
introduces
last_date_before_Gregorian, first_date_of_Gregorian: -> D
asserts
equations
last_date_before_Gregorian < first_date_of_Gregorian
% @(#)$Id: JulianGregorian.lsl,v 1.2 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: Julian and Gregorian calendar dates
%
% Source: The World Almanac and Book of facts 1993 (Pharos Books), p. 274.
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
JulianGregorian(D): trait
includes WesternMonth, Between(Int), Between(D)
assumes GregorianAssumptions(D)
introduces
leap_year: Int -> Bool
legal_day, legal_month, legal_date: D -> Bool
asserts
\forall d: D, i,j,k,y: Int
leap_year(y) == ((mod(y,4) = 0) /\
((y <= first_date_of_Gregorian.year) \/
((mod(y,400) = 0) \/ not(mod(y,100) = 0))));
days_in_month(February, y) == if leap_year(y) then 29 else 28;
legal_day(d) == between(1, d.day, days_in_month(d.month, d.year));
legal_month(d) == between(1, d.month, 12);
legal_date(d) == legal_month(d) /\ legal_day(d)
/\ (between(last_date_before_Gregorian,
d,
first_date_of_Gregorian)
=> (d = last_date_before_Gregorian
\/ d = first_date_of_Gregorian))
implies
converts leap_year, days_in_month, legal_day, legal_month, legal_date
% @(#)$Id: JulianGregorianNext.lsl,v 1.1 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: incrementing Julian and Gregorian calendar dates
%
% These functions map legal dates to legal dates
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
JulianGregorianNext(D): trait
includes JulianGregorian(D)
assumes GregorianAssumptions(D)
introduces
next_year, next_month, next_day: D -> D
asserts
\forall d: D, i,j,k,y: Int
next_year(d) == if legal_date([d.year + 1, d.month, d.day])
\/ not(legal_date(d))
then [d.year + 1, d.month, d.day]
else if not(legal_day([d.year + 1, d.month, d.day]))
then % 1 year from February 29 will be called Feb. 28th
[d.year + 1, d.month,
days_in_month(d.month, d.year + 1)]
else % d is 1 year before a day lost in switchover
first_date_of_Gregorian;
next_month(d) == if legal_date([d.year, d.month + 1, d.day])
\/ not(legal_date(d))
then [d.year, d.month + 1, d.day]
else if not(legal_month([d.year, d.month + 1, d.day]))
then % 1 month from December 31 is January 31
[d.year + 1, January, d.day]
else if not(legal_day([d.year, d.month + 1, d.day]))
then % 1 month from October 31 will be November 30
[d.year, d.month + 1,
days_in_month(d.month, d.year)]
else % d is 1 month before a day lost in switchover
first_date_of_Gregorian;
next_day(d) == if legal_date([d.year, d.month, d.day + 1])
\/ not(legal_date(d))
then [d.year, d.month, d.day + 1]
else if not(legal_day([d.year, d.month, d.day + 1]))
then % the first of the next month
next_month([d.year, d.month, 1])
else % d is last_date_before_Gregorian
first_date_of_Gregorian
% @(#)$Id: EnglishDate.lsl,v 1.2 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: Dates for the Julian and Gregorian calendar in England & Empire
%
% This reflects the change to the Gregorian calendar made in, what was in
% 1752 the British Empire. (This includes what is now the U.S.A.)
% Source: The World Almanac and Book of facts 1993 (Pharos Books), p. 274.
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
EnglishDate(D): trait
includes JulianGregorianNext(D)
asserts
equations
last_date_before_Gregorian == [1752, September, 2];
first_date_of_Gregorian == [1752, September, 14]
% @(#)$Id: CatholicDate.lsl,v 1.1 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: Dates for the Julian and Gregorian calendar in
% France, Italy, Spain, Portugal, and Luxembourg.
%
% This reflects the initial proclimation of Pope Gregory XIII.
% Note it is not valid for what was then the British Empire, let alone the
% rest of the world. Other European states swiched shortly after:
% German Catholic states, Belgium, and parts of Switzerland "within 2 years".
% Hungary changed in 1587.
% Source: The World Almanac and Book of facts 1993 (Pharos Books), p. 274.
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
CatholicDate(D): trait
includes JulianGregorianNext(D)
asserts
equations
last_date_before_Gregorian == [1582, October, 4];
first_date_of_Gregorian == [1752, October, 15]
% @(#)$Id: RussianDate.lsl,v 1.1 1994/11/15 02:38:14 leavens Exp leavens $
% SYNOPSIS: Dates for the Julian and Gregorian calendar in Russia
%
% Source: The World Almanac and Book of facts 1993 (Pharos Books), p. 274.
%
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
RussianDate(D): trait
includes JulianGregorianNext(D)
asserts
equations
last_date_before_Gregorian == [1918, January, 31];
first_date_of_Gregorian == [1918, February, 14]
% @(#)$Id: Between.lsl,v 1.1 1994/11/15 01:27:58 leavens Exp leavens $
% AUTHOR: Gary T. Leavens (leavens@cs.iastate.edu)
Between(N): trait
assumes PreOrder(<=, N)
introduces
between: N, N, N -> Bool
asserts
forall i,j,k: N
between(i,j,k) == (i <= j /\ j <= k)
Reference(s):