class Date {
private:
	uint year, month, day;
	invariant() {
		assert(1 <= month && month <= 12);
		switch (day) {
		case 29:
			assert(month ! = 2 | | leapYear(year) );
			break;
		case 30:
			assert(month ! = 2);
			break;
		case 31:
			assert(longMonth(month) );
			break;
		default:
			assert(1 <= day && day <= 28);
			break;
		}
		// no restriction on year
	}
	// Helper functions
	static pure bool leapYear(uint y) {
		return (y % 4) == 0 && (y % 100 | | (y % 400) == 0);
	}
	static pure bool longMonth(uint m) {
		return ! (m & 1) == (m > 7);
	}
public:
	. . .
}