products/sources/formale Sprachen/VDM/VDMPP/SSlibE2PP image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: metric_continuity.prf   Sprache: VDM

Original von: VDM©

class CalendarT is subclass of TestDriver 
functions
public tests : () -> seq of TestCase
tests() == 
 [
 new CalendarT12(),
 new CalendarT11(),
 new CalendarT10(),
 new CalendarT09(),
 --new CalendarT08(), --deleted
 new CalendarT07(),
 new CalendarT06(),
 new CalendarT05(),
 new CalendarT03(),
 new CalendarT02(), 
 new CalendarT01(),
 new CalendarT04()
 ];
end CalendarT

class CalendarT01 is subclass of TestCase
operations 
protected test: () ==> bool
 test() == 
  let jc = new JapaneseCalendar() in
 (
 jc.setToday(jc.getDateFrom_yyyy_mm_dd(2001,9,12));
 return
  jc.getDateFrom_yyyy_mm_dd(2003, 3, 0).asString() = "20030228" and
  jc.getDateFrom_yyyy_mm_dd(2003, 2, 29).asString() = "20030301" and
  jc.getDateFrom_yyyy_mm_dd(2004, 3, 0).asString() = "20040229" and
  jc.getDateFrom_yyyy_mm_dd(2004, 2, 30).asString() = "20040301" and
  jc.getDateFrom_yyyy_mm_dd(2004, 1, 60).asString() = "20040229" and
  jc.getDateFrom_yyyy_mm_dd(2004, 1, 61).asString() = "20040301" and
  jc.getDateFrom_yyyy_mm_dd(2001,5,1).get_yyyy_mm_dd() = mk_(2001,5,1) and
  jc.getYyyymmdd(jc.today()) = mk_(2001,9,12) and
  jc.modifiedJulianDate2Date(jc.julianDate2ModifiedJulianDate(2299160)).get_yyyy_mm_dd() = mk_(1582,10,4)  and --theDayBeforeGregorioCalendarStarted
  jc.modifiedJulianDate2Date(jc.julianDate2ModifiedJulianDate(2299160)).plus(1).get_yyyy_mm_dd() = mk_(1582,10,15) and --theFirstDayOfGregorioCalendar
  jc.date2Str(jc.getDateFromString("20010711")) = "20010711" and
  jc.convertDateFromString("saharashin") = nil and
  JapaneseCalendar`getJapaneseDateStr(jc.getDateFrom_yyyy_mm_dd(2001,5,1)) = "13 5 1" and
  jc.getAutumnalEquinox(2001).EQ(jc.getDateFrom_yyyy_mm_dd(2001,9,23)) = true
 )
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT01:\tMake date.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT01

class CalendarT02 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar() in
 return
  jc.dateAdding(jc.getDateFrom_yyyy_mm_dd(2001,5,1),3) .date2Str() = "20010504" and
  jc.diffOfDates(jc.getDateFrom_yyyy_mm_dd(2001,5,8),jc.getDateFrom_yyyy_mm_dd(2001,5,1)) = 7 and
  jc.dateSubtracting(jc.getDateFrom_yyyy_mm_dd(2001,5,1),1) .get_yyyy_mm_dd() = mk_(2001,4,30)
;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT02:\tAddition and subtraction of date.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT02

class CalendarT03 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar() in
 return
  jc.getVernalEquinox(2001).date2Str() = "20010320" and
  jc.getSummerSolstice(2001).date2Str() = "20010621" and
  jc.getAutumnalEquinox(2001).date2Str() = "20010923" and
  jc.getWinterSolstice(2001).date2Str() = "20011222" and
  jc.getVernalEquinox(2999).date2Str() = "29990320" and
  jc.getSummerSolstice(2999).date2Str() = "29990620" and
  jc.getAutumnalEquinox(2999).date2Str() = "29990922" and
  jc.getWinterSolstice(2999).date2Str() = "29991222" and
  --jc.getWinterSolstice(2008).date2Str() = "20081221" and -- error in leap year
  jc.getWinterSolstice(2007).date2Str() = "20071222" and
  jc.getWinterSolstice(2012).date2Str() = "20121221" and
  jc.getWinterSolstice(2016).date2Str() = "20161221" 
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT03:\tCalculation of Vernal Equinox, Summer Solstice, Autumnal Equinox, Winter Solstice.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT03

class CalendarT04 is subclass of TestCase
operations 
public test: () ==> bool
test() == 
 let jc = new JapaneseCalendar(),
  setOfDayOffIn2009 = jc.getSetOfDayOff(2009),
  setOfDayOff = jc.getSetOfDayOff(2001),
  setOfDayOff2003 = jc.getSetOfDayOff(2003),
  d0401 = jc.getDateFromString("20010401"),
  d0408 = jc.getDateFromString("20010408"),
  d0430 = jc.getDateFromString("20010430"),
  setOfDayOffBy_yyyy_mm_dd =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOff},
  setOfDayOffBy_yyyy_mm_dd2003 =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOff2003},
  setOfDayOffBy_yyyy_mm_ddIn2009 =  {jc.getYyyymmdd(dayOff) | dayOff in set setOfDayOffIn2009}
  in
 return
  setOfDayOffBy_yyyy_mm_dd = 
   { mk_( 2001,1,1 ),
     mk_( 2001,1,8 ),
   mk_( 2001,2,11 ),
    mk_( 2001,2,12 ),
     mk_( 2001,3,20 ),
    mk_( 2001,4,29 ),
     mk_( 2001,4,30 ),
     mk_( 2001,5,3 ),
     mk_( 2001,5,4 ),
     mk_( 2001,5,5 ),
    mk_( 2001,7,20 ),
     mk_( 2001,9,15 ),
   mk_( 2001,9,23 ),
     mk_( 2001,9,24 ),
     mk_( 2001,10,8 ),
     mk_( 2001,11,3 ),
     mk_( 2001,11,23 ),
     mk_( 2001,12,23 ),
     mk_( 2001,12,24 )
     } and
    setOfDayOffBy_yyyy_mm_dd2003 =
     { mk_( 2003,1,1 ),
     mk_( 2003,1,13 ),
     mk_( 2003,2,11 ),
     mk_( 2003,3,21 ),
     mk_( 2003,4,29 ),
     mk_( 2003,5,3 ),
     mk_( 2003,5,4 ),
     mk_( 2003,5,5 ),
     mk_( 2003,7,21 ),
     mk_( 2003,9,15 ),
     mk_( 2003,9,23 ),
     mk_( 2003,10,13 ),
     mk_( 2003,11,3 ),
     mk_( 2003,11,23 ),
     mk_( 2003,11,24 ),
      mk_( 2003,12,23 ) 
     } and
  setOfDayOffBy_yyyy_mm_ddIn2009 =
     { mk_( 2009, 1, 1 ),
    mk_( 2009, 1, 12 ),
    mk_( 2009, 2, 11 ),
    mk_( 2009, 3, 20 ),
    mk_( 2009, 4, 29 ),
    mk_( 2009, 5, 3 ),
    mk_( 2009, 5, 4 ),
    mk_( 2009, 5, 5 ),
    mk_( 2009, 5,6 ),
    mk_( 2009, 7, 20 ),
    mk_( 2009, 9, 21 ),
      mk_( 2009, 9, 22 ),
    mk_( 2009, 9, 23 ),
    mk_( 2009, 10, 12 ),
    mk_( 2009, 11, 3 ),
    mk_( 2009, 11, 23 ),
    mk_( 2009, 12, 23 ) } and
    jc.getDayOffsExceptSunday(d0401,d0430)  = 2 and
    card jc.getDayOffsAndSunday(d0401,d0430) = 1 and
    jc.getDayOffsAndSunday(d0401,d0408) = {}
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT04:\tGet set of Day off.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT04

class CalendarT05 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar(),
  d0711 = jc.getDateFromString("20010711"in
 (
 jc.setToday(jc.getDateFrom_yyyy_mm_dd(2001,3,1));
 let d0301 = jc.today() in
 return
  d0711.EQ(jc.getDateFrom_yyyy_mm_dd(2001, 7, 11)) and
  jc.EQ(d0711,jc.getDateFrom_yyyy_mm_dd(2001, 7, 11)) and
  d0301.LT(d0711) and
  jc.LT(d0301, d0711) and
  d0711.GT(d0301) and
  jc.GT(d0711,d0301) and
  d0711.GE(d0711) and d0711.GE(d0301) and
  jc.GE(d0711,d0711)  and jc.GE(d0711,d0301) and
  d0711.LE(d0711) and d0301.LE(d0711) and
  jc.LE(d0711,d0711) and jc.LE(d0301,d0711) 
 )
;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT05:\tCompare date.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT05

class CalendarT06 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar(),
  d10010301 = jc.getDateFromString("10010301"),
  d0711 = jc.getDateFromString("20010711")  in
 (
 let d0301 = jc.today() in
 return
  jc.firstDayOfTheWeekInMonth(2000,3,<Wed>).get_yyyy_mm_dd() = mk_( 2000,3,1 ) and
  jc.firstDayOfTheWeekInMonth(2001,7,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,1 ) and
  jc.lastDayOfTheWeekInMonth(2000,2,<Tue>).get_yyyy_mm_dd() = mk_( 2000,2,29 ) and
  jc.lastDayOfTheWeekInMonth(2001,7,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,29 ) and
  jc.getNthDayOfTheWeek(2001,7,5,<Sun>).get_yyyy_mm_dd() = mk_( 2001,7,29 ) and
  jc.getNthDayOfTheWeek(2001,7,6,<Sun>) = false and
  jc.getNumberOfTheDayOfWeek(d0711,d0301,<Sun>)  = 19 and
  jc.getNumberOfTheDayOfWeek(d0711,d10010301,<Sun>)  = 52196 and
  jc.getNumberOfDayOfTheWeekFromName(<Thu>) = 4 and
  jc.getNumberOfDayOfTheWeekFromName(<Fri>) = 5 and
  jc.getNumberOfDayOfTheWeekFromName(<Sat>) = 6 and
  jc.getNumberOfDayOfTheWeekFromName(<Sun>) = 0 
 )
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT06:\tGet day of the week.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT06

class CalendarT07 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar() in
 return
  jc.getDateFromString("sahara") = false and
  jc.getDateFromString("20011232") = false and
  jc.getDateFromString("20011231").date2Str() = "20011231"
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT07:\tgetDateFromString";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT07

class CalendarT09 is subclass of TestCase, CalendarDefinition
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar()
 in
 return
  jc.today().EQ(jc.getDateFrom_yyyy_mm_dd(2001, 3, 1)) and
  jc.readFromFiletoday(homedir ^ "/temp/BaseDay.txt").EQ(jc.getDateFrom_yyyy_mm_dd(2003, 10, 24))
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT09:\tRead today datefrom a file.";
protected tearDown: () ==> ()
tearDown() == return;

end CalendarT09

class CalendarT10 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar()
 in
 return
  jc.getLastDayOfMonth(2004, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 31)) and
  jc.getLastDayOfMonth(2004, 2).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
  jc.getLastDayOfMonth(2004, 3).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 3, 31)) and
  jc.getLastDayOfMonth(2004, 4).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 4, 30)) and
  jc.getLastDayOfMonth(2004, 5).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 5, 31)) and
  jc.getLastDayOfMonth(2004, 6).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 6, 30)) and
  jc.getLastDayOfMonth(2004, 7).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 7, 31)) and
  jc.getLastDayOfMonth(2004, 8).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 8, 31)) and
  jc.getLastDayOfMonth(2004, 9).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 9, 30)) and
  jc.getLastDayOfMonth(2004, 10).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 10, 31)) and
  jc.getLastDayOfMonth(2004, 11).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 11, 30)) and
  jc.getLastDayOfMonth(2004, 12).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 12, 31)) and
  jc.getLastDayOfMonth(2003, 13).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 31)) and
  jc.getLastDayOfMonth(2003, 8+6).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
  jc.getLastDayOfMonth(2003, 15).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 3, 31)) and
  jc.getLastDayOfMonth(2003, 16).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 4, 30)) and
  jc.getLastDayOfMonth(2003, 17).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 5, 31)) and
  jc.getLastDayOfMonth(2003, 18).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 6, 30)) and
  jc.getLastDayOfMonth(2003, 19).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 7, 31)) and
  jc.getLastDayOfMonth(2003, 20).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 8, 31)) and
  jc.getLastDayOfMonth(2003, 21).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 9, 30)) and
  jc.getLastDayOfMonth(2003, 22).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 10, 31)) and
  jc.getLastDayOfMonth(2003, 23).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 11, 30)) and
  jc.getLastDayOfMonth(2003, 24).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 12, 31)) and
  jc.getLastDayOfMonth(2005, 2).EQ(jc.getDateFrom_yyyy_mm_dd(2005, 2, 28))
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT10:\tGet the end of month.";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT10

class CalendarT11 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar()
 in
 return
  jc.getRegularDate(2004, 1, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 1)) and
  jc.getRegularDate(2003, 12, 32).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 1)) and
  jc.getRegularDate(2003, 24, 32).EQ(jc.getDateFrom_yyyy_mm_dd(2005, 1, 1)) and
  jc.getRegularDate(2003, 13, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 1)) and
  jc.getRegularDate(2004, 1, 32).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 1)) and
  jc.getRegularDate(2004, 2, 0).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 1, 31)) and
  jc.getRegularDate(2004, 2, 28).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 28)) and
  jc.getRegularDate(2004, 2, 29).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
  jc.getRegularDate(2004, 3, 0).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 29)) and
  jc.getRegularDate(2004, 3, -1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 2, 28)) and
  jc.getRegularDate(2003, 2, 29).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 3, 1)) and
  jc.getRegularDate(2004, 4, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2004, 4, 1)) and
  jc.getRegularDate(2004, 0, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 12, 1)) and
  jc.getRegularDate(2004, -1, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 11, 1)) and
  jc.getRegularDate(2004, -10, 29).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 3, 1)) and
  jc.getRegularDate(2004, -10, 28).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 2, 28)) and
  jc.getRegularDate(2004, -11, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2003, 1, 1)) and
  jc.getRegularDate(2004, -12, 1).EQ(jc.getDateFrom_yyyy_mm_dd(2002, 12, 1))
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT11:\tgetRegularDate";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT11

class CalendarT12 is subclass of TestCase
operations 
protected test: () ==> bool
test() == 
 let jc = new JapaneseCalendar()
 in
 return
  jc.getRegularMonth(2004, 1) = mk_(2004, 1) and
  jc.getRegularMonth(2004, 2) = mk_(2004, 2) and
  jc.getRegularMonth(2004, 3) = mk_(2004, 3) and
  jc.getRegularMonth(2004, 4) = mk_(2004, 4) and
  jc.getRegularMonth(2004, 5) = mk_(2004, 5) and
  jc.getRegularMonth(2004, 6) = mk_(2004, 6) and
  jc.getRegularMonth(2004, 7) = mk_(2004, 7) and
  jc.getRegularMonth(2004, 8) = mk_(2004, 8) and
  jc.getRegularMonth(2004, 9) = mk_(2004, 9) and
  jc.getRegularMonth(2004, 10) = mk_(2004, 10) and
  jc.getRegularMonth(2004, 11) = mk_(2004, 11) and
  jc.getRegularMonth(2004, 12) = mk_(2004, 12) and
  jc.getRegularMonth(2004, 13) = mk_(2005, 1)  and
  jc.getRegularMonth(2004, 14) = mk_(2005, 2) and
  jc.getRegularMonth(2004, 24) = mk_(2005, 12) and
  jc.getRegularMonth(2004, 25) = mk_(2006, 1) and
  jc.getRegularMonth(2004, 0) = mk_(2003, 12) and
  jc.getRegularMonth(2004, -1) = mk_(2003, 11) and
  jc.getRegularMonth(2004, -10) = mk_(2003, 2) and
  jc.getRegularMonth(2004, -11) = mk_(2003, 1) and
  jc.getRegularMonth(2004, -12) = mk_(2002, 12) and
  jc.getRegularMonth(2004, -13) = mk_(2002, 11)
 ;
protected setUp: () ==> ()
setUp() == TestName := "CalendarT12:\tgetRegularMonth";
protected tearDown: () ==> ()
tearDown() == return;
end CalendarT12

¤ Dauer der Verarbeitung: 0.33 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff