| Previous | Table of Contents | Next |
[C-1] month must be specified when recurringType is everyYear. context RecurringPointInTimeEvent inv: self.recurringType=everyYear
implies self.month->notEmpty
[C-2] month must be between 1 and 12 (inclusive) when specified. context RecurringPointInTimeEvent inv: self.month->notEmpty
implies 1 <= self.month <= 12
[C-3] dayOfMonth must be specified when recurringType is everyYear or everyMonth.
context RecurringPointInTimeEvent
inv: self.recurringType=everyYear or self.recurringType=everyMonth implies self.dayOfMonth->notEmpty
[C-4] dayOfMonth must be between 1 and 31 (inclusive) when specified. context RecurringPointInTimeEvent inv: self.dayOfMonth->notEmpty
implies 1 <= self.dayOfMonth <= 31
[C-5] dayOfWeek must be specified when recurringType is everyWeek. context RecurringPointInTimeEvent inv: self.recurringType=everyWeek
implies self.dayOfWeek->notEmpty
[C-6] hour must be specified when recurringType is everyYear or everyMonth or everyWeek or everyDay.
context RecurringPointInTimeEvent
inv: self.recurringType=everyYear or self.recurringType=everyMonth or self.recurringType=everyWeek or self.recurringType=everyDay
implies self.hour->notEmpty
[C-7] hour must be between 0 and 23 (inclusive) when specified. context RecurringPointInTimeEvent inv: self.hour->notEmpty
implies 0 <= hour <= 23
[C-8] minute must be specified when recurringType is not everyMinute. context RecurringPointInTimeEvent inv: self.recurringType<>everyMinute
implies self.minute->notEmpty
[C-9] minute must be between 0 and 59 (inclusive) when specified. context RecurringPointInTimeEvent inv: self.minute->notEmpty
implies 0 <= self.minute <= 59
[C-10] second must be between 0 and 59 (inclusive). context RecurringPointInTimeEvent inv: 0 <= self.second <= 59