Quelle Calendar.vdmpp Sprache: VDM

class CalendarDefinition
values
public homedir = ".";
types
public NameOfDayOfTheWeek = <Mon> | <Tue> | <Wed> | <Thu> | <Fri> | <Sat> | <Sun>;
public NumberOfDayOfTheWeek = nat
inv d == d <= 6; --number of day of the week (Sunday=0, Saturday=6);

end CalendarDefinition
--------------------------------------------------------------
class Calendar is subclass of CalendarDefinition -- Gregorio Calendar
/*
Responsibility
I am a Gregorio Calendar.
Abstract
I calculate Gregorio Calendar by cooperating with Date class.
You can get the the vernal equinox and the autumnal equinox until year 2099.
My subclass has to define the set of holiday.
My calculation is based on GMT, so my subclass has to calculate the diofference to GMT.
*/

values
--difference of julianDate and modifiedJulianDate
private daysDifferenceOfModifiedJulianDate = 2400000.5;

private namesOfDayOfTheWeek = [<Sun>,<Mon>,<Tue>,<Wed>,<Thu>,<Fri>,<Sat>];

private daysInYear = 365.25;
protected monthsInYear = 12;
private correctedMonths = 14;
private daysInWeek = 7;
private averageDaysInMonth = 30.6001;
private yearInCentury = 100;
private calculationCoefficientOfDate = 122.1;
private calculationCoefficientOfYear = 4800;
private centuryCalculationCoefficient = 32044.9;
private theDayBeforeGregorioCalendarStarted  = 2299160.0;
private theFirstDayOfGregorioCalendar  = 1582.78;

io = new IO();

instance variables

protected differenceWithGMT : real := 0;
protected iToday : [Date] := nil;
protected Year2Holidays : map int to set of Date := { |-> }; -- { year |-> set of holidays }

functions

----Comparing magnitude functions

public LT: Date * Date -> bool
LT(date1, date2) == date1.getModifiedJulianDate() < date2.getModifiedJulianDate();

public GT: Date * Date -> bool
GT(date1,date2) == date1.getModifiedJulianDate() > date2.getModifiedJulianDate();

public LE: Date * Date -> bool
LE(date1,date2) == not GT(date1,date2);

public GE: Date * Date -> bool
GE(date1,date2) == not LT(date1,date2);

-- Is date1 value equal date2 value?
public EQ: Date * Date -> bool
EQ(date1,date2) == date1.getModifiedJulianDate() = date2.getModifiedJulianDate();

public min : Date -> Date -> Date
min(date1)(date2) == if date1.LT(date2) then date1 else date2;

public max : Date -> Date -> Date
max(date1)(date2) == if date1.GT(date2) then date1 else date2;

----Query

public isDateString :
seq of char -- date string (yyyymmdd format)
->
bool  -- if correct date then true else false
isDateString(yyyymmdd) == if getDateFromString(yyyymmdd) = false then false else true;

-- is leap year?
public isLeapYear:
int -- year
->
bool -- leap year or not
isLeapYear(year) == year mod 400 = 0 or (year mod yearInCentury <> 0 and year mod 4 = 0);

public getNumberOfDayOfTheWeek: Date -> NumberOfDayOfTheWeek
getNumberOfDayOfTheWeek(date) ==
let modifiedJulianDate = floor(date.getModifiedJulianDate())
in (modifiedJulianDate - 4) mod daysInWeek;

public getYyyymmdd: Date -> int * int * int
getYyyymmdd(date) == mk_(Year(date),Month(date),day(date));

public getNameOfDayOfTheWeek : Date -> NameOfDayOfTheWeek
getNameOfDayOfTheWeek(date) == namesOfDayOfTheWeek(getNumberOfDayOfTheWeek(date) + 1);

public getNumberOfDayOfTheWeekFromName : NameOfDayOfTheWeek -> NumberOfDayOfTheWeek
getNumberOfDayOfTheWeekFromName(nameOfDayOfTheWeek) == Sequence`Index[Calendar`NameOfDayOfTheWeek](nameOfDayOfTheWeek)(namesOfDayOfTheWeek) - 1;

public firstDayOfTheWeekInMonth : int * int * NameOfDayOfTheWeek -> Date
firstDayOfTheWeekInMonth(year, month,nameOfDayOfTheWeek) ==
let numberOfDayOfTheWeek = getNumberOfDayOfTheWeekFromName(nameOfDayOfTheWeek),
  firstDayOfMonth = getFirstDayOfMonth(year, month),
  diff = numberOfDayOfTheWeek - getNumberOfDayOfTheWeek(firstDayOfMonth) in
cases true:
  (diff = 0) -> firstDayOfMonth,
  (diff > 0) -> firstDayOfMonth.plus(diff),
  (diff < 0) -> firstDayOfMonth.plus((daysInWeek + diff) mod daysInWeek)
end;

-- Get the last date which has the specified name of day of the week
-- My algorithm thinks "year Y, month 13" = "year y+1, month 1", so I can month + 1
public lastDayOfTheWeekInMonth : int * int * NameOfDayOfTheWeek -> Date
lastDayOfTheWeekInMonth(year, month, nameOfDayOfTheWeek) == firstDayOfTheWeekInMonth(year,(month+1),nameOfDayOfTheWeek).minus(daysInWeek);

-- Get the n-th day of the week of specified month
public getNthDayOfTheWeek : int * int * int * NameOfDayOfTheWeek
->
Date | bool  -- the date which has n-th  day of the week, if not exist then false
getNthDayOfTheWeek(aYear, aMonth, n, nameOfDayOfTheWeek) ==
let firstDayOfMonth = firstDayOfTheWeekInMonth(aYear,aMonth,nameOfDayOfTheWeek),
  r = firstDayOfMonth.plus(daysInWeek * (n - 1)) in
cases Month(r):
  (aMonth) -> r,
  others -> false
end;

--new Calendar().getFirstDayOfMonth(2001,7).get_yyyy_mm_dd() = mk_( 2001,7,1 )
public getFirstDayOfMonth : int * int -> Date
getFirstDayOfMonth(year, month) == getRegularDate(year, month, 1);

--new Calendar().getLastDayOfMonth(2001,7).get_yyyy_mm_dd() = mk_( 2001,7,31 )
public getLastDayOfMonth : int * int -> Date
getLastDayOfMonth(year, month) == getRegularDate(year, month+1, 1).minus(1);

public isSunday : Date -> bool
isSunday(date) == getNumberOfDayOfTheWeek(date) = 0;

public isSaturday : Date -> bool
isSaturday(date) == getNumberOfDayOfTheWeek(date) = 6;

public isWeekday : Date -> bool
isWeekday(date) == getNumberOfDayOfTheWeek(date) in set {1,...,5};

public isNotDayOff : Date -> bool
isNotDayOff(date) == not isSundayOrDayoff(date);

public isWeekday : NameOfDayOfTheWeek -> bool
isWeekday(nameOfDayOfTheWeek) == nameOfDayOfTheWeek not in set {<Sat>,<Sun>};

-- Return how many days between date1 and date2 of nameOfDayOfTheWeek.
-- include date1 and date2 iff they have the nameOfDayOfTheWeek.
public getNumberOfTheDayOfWeek: Date * Date * NameOfDayOfTheWeek -> int
getNumberOfTheDayOfWeek(date1,date2,nameOfDayOfTheWeek) ==
let numberOfDayOfTheWeek = getNumberOfDayOfTheWeekFromName(nameOfDayOfTheWeek),
  startDate = min(date1)(date2),
  endDate = max(date1)(date2),
  numOfDays = diffOfDates(endDate,startDate) + 1,
  quotient = numOfDays div daysInWeek,
  remainder = numOfDays mod daysInWeek,
  delta = if subtractDayOfTheWeek(numberOfDayOfTheWeek,getNumberOfDayOfTheWeek(startDate)) + 1 <= remainder then 1 else 0 in
quotient + delta
/*
post
let startDate = min(date1)(date2),
endDate = max(date1)(date2) in
let setOfTheDayOfTheWeek = {day | day : Date & nameOfDayOfTheWeek = getNameOfDayOfTheWeek(day )}  in
forall Date0, Date1  in set setOfTheDayOfTheWeek &
startDate.LE(Date0) and Date0.LE(Date1) and Date1.LE(endDate) =>
diffOfDates(Date1, Date0) mod 7 = 0 and
exists1 日i  in set setOfTheDayOfTheWeek &
diffOfDates(日i, startDate) < 6 and
exists1 日j  in set setOfTheDayOfTheWeek &
diffOfDates(endDate, 日j) < 6 and
diffOfDates(日j, 日i) = 7 * ((card setOfTheDayOfTheWeek) - 1)
*/
  ;
/*
Following Japanese statement are the refinement proof by Shin Sahara and Mr. Toshiharu Yamazaki.
以下は、上記関数の山崎利治さんによる段階的洗練を佐原が「翻訳」した記述

pre
type R = {|rng [n → n / 7 | n∈Int]|} -- 7で割った商の集合
f, t∈Int, w∈R, 0≦f≦t,
h: Int → R --環準同型（ring homomorphism）

post
S = dom h(w) ∩ {f..t}・RESULT ≡ card(S) -- RESULTが答え（dom h(w)≡h-1(w)）

--整数系を環（ring）と見て、その商環（quotient ring）への準同型写像があり、その代数系上で事後条件を満たすプログラムを作る
I =｛f..t}
d = t - f + 1 -- = card(I)
q = d / 7
r = d \ 7 --7で割った余り

とすると、

q ≦ A ≦ q+1

が成り立つ。なぜなら、

任意の連続する７日間には、必ずw曜日がちょうど１日存在する。
card(I) = 7×q + r (0≦r＜7)であるから、Iには少なくともq個の連続する７日間が存在するが、q+1個は存在しない。
余りのr日間にw曜日が存在するかも知れない。

次に、

x ++ y = (x + y) \ 7
x ┴ y = max(x - y, 0)
として、

T = {h(f)..h(f) ++ (r ┴ 1)}
を考える。Tは余りr日間の曜日に対応する（card(T) = r）。
すると、

A ≡ if w∈T then q + 1 els q end

ここで、

x minus y = if x ≧ y then x - y els x - y + 7 end
とすれば、

w∈T ⇔ (w minus h(f)) + 1 ≦ r
である。なぜならば

w∈T ⇔ {0..(r ┴ 1)}∋wﾕ = w minus h(f)
⇔ r ┴ 1 ≧ wﾕ
⇔ r ≧ (w minus h(f)) + 1

従って、プログラムは以下のようになる。

A(f, t w)≡
let
d ≡ t - f + 1
q ≡ d / 7
r ≡ d \ 7
delta ≡ if (w minus h(f)) + 1 ≦ r then 1 els 0 end
x minus y ≡ if x ≧ y then x - y els x - y + 7 end
in
q + delta
end
*/

private subtractDayOfTheWeek: int * int -> int
subtractDayOfTheWeek(x,y) == if x >= y then x - y else x - y + daysInWeek;

--dateから、そのdateの属するyearを求める。
public Year: Date -> int
Year(date) ==
if monthAux(date) < correctedMonths then
  yearAux(date) - calculationCoefficientOfYear
else
  yearAux(date) - calculationCoefficientOfYear + 1;

--dateから、そのdateの属するmonthを求める。
public Month: Date -> int
Month(date) == if monthAux(date) < correctedMonths then
  monthAux(date) - 1
else
  monthAux(date) - 13;

--dateから、dayを求める。
public day: Date -> int
day(date) == daysFromTheBeginningOfTheMonth(date);

--new Date().daysFromNewYear(getDateFrom_yyyy_mm_dd(2001,12,31)) = 365
public daysFromNewYear: Date -> int
daysFromNewYear(date) ==
let firstDateOfYear = getDateFrom_yyyy_mm_dd(Year(date), 1, 0)
in diffOfDates(date,firstDateOfYear);

daysFromTheBeginningOfTheMonth: Date -> int
daysFromTheBeginningOfTheMonth(date) == floor(daysFromTheBeginningOfTheMonthAsReal(date));

daysFromTheBeginningOfTheMonthAsReal: Date -> real
daysFromTheBeginningOfTheMonthAsReal(date) == yyyymmddModifyAux(date) + calculationCoefficientOfDate
- floor(daysInYear * yearAux(date)) - floor(averageDaysInMonth * monthAux(date));

monthAux:
Date
->
int --datecalculation上都合の良いMonth(4..15)を返す
monthAux(date) ==
floor((yyyymmddModifyAux(date) + calculationCoefficientOfDate - floor(daysInYear * yearAux(date))) / averageDaysInMonth);

--dateをyyyymmddに変更するためのAux。
yyyymmddModifyAux: Date -> real
yyyymmddModifyAux(date) ==
let julianDate = mjd2Jd(date.getModifiedJulianDate()),
  century =  floor((julianDate + centuryCalculationCoefficient) / 36524.25)
in
  if julianDate > theDayBeforeGregorioCalendarStarted then
   julianDate + centuryCalculationCoefficient + century - century div 4 + 0.5
  else
   julianDate + 32082.9 + 0.5;

--dateからyearを求めるためのAux。
yearAux:
Date
->
int --datecalculationに都合の良い補正したyear数。
yearAux(date) == floor (yyyymmddModifyAux(date) / daysInYear);

public getVernalEquinoxOnGMT: int -> Date
getVernalEquinoxOnGMT(year) ==
let y = year / 1000.0 in
modifiedJulianDate2Date(
  julianDate2ModifiedJulianDate(1721139.2855 + 365.2421376 * year + y * y *  (0.067919 - 0.0027879 * y)));

public getSummerSolsticeOnGMT: int -> Date
getSummerSolsticeOnGMT(year) ==
let y = year / 1000.0 in
modifiedJulianDate2Date(
  julianDate2ModifiedJulianDate(1721233.2486 + 365.2417284 * year - y * y * (0.053018 - 0.009332 * y)));

public getAutumnalEquinoxOnGMT: int -> Date
getAutumnalEquinoxOnGMT(year) ==
let y = year / 1000.0 in
modifiedJulianDate2Date(
  julianDate2ModifiedJulianDate (1721325.6978 + 365.2425055 * year - y * y * (0.126689 - 0.0019401 * y)));

public getWinterSolsticeOnGMT: int -> Date
getWinterSolsticeOnGMT(year) ==
let y = year / 1000.0 in
modifiedJulianDate2Date(
  julianDate2ModifiedJulianDate(1721414.392 + 365.2428898 * year - y * y * (0.010965 - 0.0084855 * y)));

  public getVernalEquinox : int -> Date
getVernalEquinox(year) == getDateInStandardTime(getVernalEquinoxOnGMT(year));

public getSummerSolstice : int -> Date
getSummerSolstice(year) == getDateInStandardTime(getSummerSolsticeOnGMT(year));

public getAutumnalEquinox : int -> Date
getAutumnalEquinox(year) == getDateInStandardTime(getAutumnalEquinoxOnGMT(year));

-- Now, I can't get the right Winter Solstice in leap year
public getWinterSolstice : int -> Date
getWinterSolstice(year) == getDateInStandardTime(getWinterSolsticeOnGMT(year));

----calculation

public dateAdding: Date * int -> Date
dateAdding(date,addNumOfDays) == date.plus(addNumOfDays);

public diffOfDates: Date * Date -> int
diffOfDates(date1,date2) == floor(date1.getModifiedJulianDate() - date2.getModifiedJulianDate());

--dateからnumOfDaysを減算したdateを返す
public dateSubtracting: Date * int -> Date
dateSubtracting(date,subtractNumOfDays) == date.minus(subtractNumOfDays);

----Conversion

public mjd2Jd: real -> real
mjd2Jd(modifiedJulianDate) == modifiedJulianDate + daysDifferenceOfModifiedJulianDate;

public julianDate2ModifiedJulianDate: real -> real
julianDate2ModifiedJulianDate(julianDate) == julianDate - daysDifferenceOfModifiedJulianDate;

--yyyymmddを通常の値の範囲内に変換する。
--new Calendar().getRegularDate(2003, 14, 29) = getDateFrom_yyyy_mm_dd(2004, 2, 29)
public getRegularDate : int * int * int -> Date
getRegularDate(candidateYear, candidateOfMonth, candidateDate) ==
let mk_(year, month) = getRegularMonth(candidateYear, candidateOfMonth)
in
getDateFrom_yyyy_mm_dd(year, month, candidateDate);

--年月を通常の値の範囲内に変換する。
public getRegularMonth : int * int -> int * int
getRegularMonth(candidateYear, candidateOfMonth) ==
let year =
   if candidateOfMonth <= 0 then
    candidateYear + (candidateOfMonth - 12) div monthsInYear
   else
    candidateYear + (candidateOfMonth - 1) div monthsInYear,
  candidateOfMonth2 = candidateOfMonth mod monthsInYear,
  month =
   if candidateOfMonth2 = 0 then
    12
   else
    candidateOfMonth2
in
mk_(year, month);

--（整数三つ組の）date2Year(2001,7,1) = 2001.5
public date2Year:  int * int * int
->
real --dateをYear(実数)に変換した値
date2Year(year, month, day) == year + (month - 1) / monthsInYear + (day - 1.0) / daysInYear;

public date2Str : Date +> seq of char
date2Str(date) == date.date2Str();

public convertDateFromString : seq of char +> [Date]
convertDateFromString(dateStr) ==
let date = getDateFromString(dateStr)
    in if date = false then nil
     else date;

--以下は、休日の考慮をした機能で、サブクラスで休日の集合を定義する必要がある。

/* Query */
--２つのdateの間の休日の集合を返す。日曜日である休日も含むが、休日でない日曜日は含まない。
public getSetOfDayOffBetweenDates : Date * Date -> set of Date
getSetOfDayOffBetweenDates(date1,date2) ==
let Date1 = min(date1)(date2),
  Date2 = max(date1)(date2),
  setOfYear = {Year(Date1),...,Year(Date2)},
  setOfDayOff = dunion {getSetOfDayOff(year) | year in set setOfYear}
in
{dayOff | dayOff in set setOfDayOff & date1.LE(dayOff) and dayOff.LE(date2)};

--２つのdateの間の休日の数を返す。日曜日である休日も含むが、休日でない日dayOfWeekは含まない。
public getDayOffsExceptSunday: Date * Date -> int
getDayOffsExceptSunday(date1,date2) == card (getSetOfDayOffBetweenDates(date1,date2));

--２つのdateの間の休日あるいは日曜日の数を返す（startDateを含む）
public getTheNumberOfDayOff: Date * Date -> int
getTheNumberOfDayOff(date1,date2) ==
let Date1 = min(date1)(date2),
  Date2 = max(date1)(date2),
  numberOfSunday = getNumberOfTheDayOfWeek(Date1,Date2,<Sun>) in
numberOfSunday + card getSetOfNotSundayDayOff(Date1,Date2);

--２つのdateの間の休日あるいは日曜日の数を返す（startDateを含まない）
public getTheNumberOfDayOffExceptStartDate: Date * Date -> int
getTheNumberOfDayOffExceptStartDate(date1,date2) ==
let Date1 = min(date1)(date2),
  Date2 = max(date1)(date2) in
getTheNumberOfDayOff(Date1.plus( 1), Date2);

private getSetOfNotSundayDayOff : Date * Date -> set of Date
getSetOfNotSundayDayOff(date1,date2) ==
let setOfDayOff = getSetOfDayOffBetweenDates(date1,date2) in
{dayOff | dayOff in set setOfDayOff & not isSunday(dayOff)};

--日曜日である休日の集合を返す
public getDayOffsAndSunday : Date * Date -> set of Date
getDayOffsAndSunday(date1,date2) ==
let setOfDayOff = getSetOfDayOffBetweenDates(date1,date2) in
{dayOff | dayOff in set setOfDayOff & isSunday(dayOff)};

/* Conversion */

--休日でないdateを返す（未来へ向かって探索する）
public getFutureWeekday : Date-> Date
getFutureWeekday(date) ==
cases  isSundayOrDayoff(date) or isSaturday(date):
  (true) -> getFutureWeekday(date.plus( 1)),
  others -> date
end
measure getFutureWeekdayMeasure;

getFutureWeekdayMeasure : Date +> nat
getFutureWeekdayMeasure(d) == -d.getModifiedJulianDate();

--休日でないdateを返す（過去へ向かって探索する）
public getPastWeekday : Date-> Date
getPastWeekday(date) ==
cases   isSundayOrDayoff(date) or isSaturday(date):
  (true) -> getPastWeekday (date.minus(1)),
  others -> date
end
measure getPastWeekdaymeasure;

getPastWeekdaymeasure : Date +> nat
getPastWeekdaymeasure(d) == d.getModifiedJulianDate();

--与えられた平日に、平日n日分を加算する
public addWeekday : Date * int -> Date
addWeekday(date,addNumOfDays) == addWeekdayAux(getFutureWeekday(date),addNumOfDays);

public addWeekdayAux : Date * int -> Date
addWeekdayAux(date,addNumOfDays) ==
cases isSundayOrDayoff(date) or isSaturday(date):
  (true) -> addWeekdayAux(date.plus(1),addNumOfDays),
  others ->
     if addNumOfDays <= 0 then
      date
     else
      addWeekdayAux(date.plus(1), addNumOfDays-1)
end
measure restOfNumberOfDay;

restOfNumberOfDay : Date * int +> nat
restOfNumberOfDay(-, numOfDays) == if numOfDays <= 0 then 0 else numOfDays - 1;

--与えられた平日に、平日n日分を減算する
public subtractWeekday : Date * int -> Date
subtractWeekday(date,subtractNumOfDays) == subtractWeekdayAux(getPastWeekday(date),subtractNumOfDays);

public subtractWeekdayAux : Date * int -> Date
subtractWeekdayAux(date,subtractNumOfDays) ==
cases isSundayOrDayoff(date) or isSaturday(date):
  (true) -> subtractWeekdayAux(date.minus(1),subtractNumOfDays),
  others ->
     if subtractNumOfDays <= 0 then
      date
     else
      subtractWeekdayAux(date.minus(1), subtractNumOfDays-1)
end
measure restOfNumberOfDay;

/* Query */

public isDayOff : Date -> bool
isDayOff(date) ==
let setOfDayOff = {d.getModifiedJulianDate() | d in set getSetOfDayOff(date.Year())} in
date.getModifiedJulianDate() in set setOfDayOff;

public isSundayOrDayoff : Date -> bool
isSundayOrDayoff(date) ==  isSunday(date) or isDayOff(date);

public isInDateSet :  Date * set of Date -> bool
isInDateSet(date, aNationalHolidaySet) == (
let holidaySetByModifiedJulianDate = {floor d.getModifiedJulianDate() | d in set aNationalHolidaySet}
in
date.getModifiedJulianDate() in set holidaySetByModifiedJulianDate
  );

operations

public modifiedJulianDate2Date: real ==> Date
modifiedJulianDate2Date(modifiedJulianDate) ==
return new Date(self,modifiedJulianDate);

public getDateFrom_yyyy_mm_dd: int * int * int  ==> Date
getDateFrom_yyyy_mm_dd(year, month, day) ==
let [y,m] = if (month > correctedMonths - monthsInYear) then
   [year + calculationCoefficientOfYear , month + 1]
  else
   [year + calculationCoefficientOfYear - 1 , month + correctedMonths - 1],
  century = y div yearInCentury,
   centuryCoefficient =  if (date2Year(year, month, day) > theFirstDayOfGregorioCalendar) then
      century div 4 - century - 32167.0
     else
      -32205.0,
  haldDay = 0.5
in
return
  modifiedJulianDate2Date(floor(daysInYear * y) +
  floor(averageDaysInMonth * m) + day + centuryCoefficient - haldDay - daysDifferenceOfModifiedJulianDate);

public getDateFromString :
seq of char --yyyymmdd
==>
Date | bool -- if not date then false
getDateFromString(yyyymmdd) ==
(if not String`isDigits(yyyymmdd) then
  return false;
let yyyymmddByInt = String`asInteger(yyyymmdd),
  year = yyyymmddByInt div 10000,
  mmddByInt = yyyymmddByInt mod 10000,
  month =  mmddByInt div 100,
  day =  mmddByInt mod 100
in
  if getDateFrom_yyyy_mm_dd(year,month,day).date2Str() = yyyymmdd then
   return getDateFrom_yyyy_mm_dd(year,month,day)
  else
   return false
);

public getDateInStandardTime : Date ==> Date
getDateInStandardTime(date) ==
return modifiedJulianDate2Date (date.getModifiedJulianDate() + date.calendar().getDifferenceWithGMT());

public getDayOfTheWeekInYear : int * NameOfDayOfTheWeek ==> set of Date
getDayOfTheWeekInYear(year,dayOfWeek) ==
(
dcl aSetOfTheDayOfWeek : set of Date := {},
  date : Date := self.getNthDayOfTheWeek(year,1,1,dayOfWeek);
while date.LE(self.lastDayOfTheWeekInMonth(year,12,dayOfWeek)) do (
   aSetOfTheDayOfWeek :=  aSetOfTheDayOfWeek union {date};
  date := date.plus(7)
);
return aSetOfTheDayOfWeek
);

public getDifferenceWithGMT : () ==> real
getDifferenceWithGMT() == return differenceWithGMT;

public setDifferenceWithGMT : (real) ==> ()
setDifferenceWithGMT(diff) == differenceWithGMT := diff;

public setTheSetOfDayOffs: int ==> ()
setTheSetOfDayOffs(-) == is subclass responsibility;

public getSetOfDayOff: int ==> set of Date
getSetOfDayOff(aYear) ==
(
if not aYear in set dom Year2Holidays then
  self.setTheSetOfDayOffs(aYear);
return self.Year2Holidays(aYear)
);

--read todayfrom a file
public readToday : seq of char ==> [Date]
readToday(fname) ==
let mk_(r, mk_(y, m, d)) = io.freadval[int * int * int](fname)
in
if r then
  return getDateFrom_yyyy_mm_dd(y,m,d)
else
  let - = io.echo("Can't read today's data file.")
  in
  return nil;

--stub functions for getting today
public today: () ==> Date
today() ==
if iToday = nil then
  return readToday(homedir ^ "/temp/Today.txt")
else
  return iToday;

--todayのdateを指定したreadFromFile。
public readFromFiletoday: seq of char ==> Date
readFromFiletoday(fname) ==
if iToday = nil then
  return readToday(fname)
else
  return iToday;

public setToday : Date ==> ()
setToday(date) == iToday := date;

public todayOnBusiness: () ==> Date
todayOnBusiness() == is subclass responsibility;

public setTodayOnBusiness : Date ==> ()
setTodayOnBusiness(-) == is subclass responsibility;

public todayOnCompany:  seq of char ==> Date
todayOnCompany(companyCode) == is subclass responsibility;

public setTodayOnCompany : seq of char * Date ==> ()
setTodayOnCompany(companyCode,-) == is subclass responsibility;

end Calendar

quality99%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.