| View: | Hide Browser | Browser on the left | Browser on the right | Dictionary |
| Report: | General Info |
| General Info | |
| Name | Enclosing_interval |
| Expression | inv: month_known implies enclosing_interval.lower.day = 1 and enclosing_interval.upper.day = days_in_month(month, year) and not month_known implies enclosing_interval.lower.month = 1 and enclosing_interval.upper.month = Months_in_year and enclosing_interval.lower.day = 1 and enclosing_interval.upper.day = days_in_month(Months_in_year, year) |
| Base Classes | Class |