invariant(1 <= day && day <= 31);