Is DV_INTERVAL missing invariants?

Specifications
1

Reading the RM 1.1.0 data types spec, in DV_INTERVAL and Interval types I think we are missing an invariant, for instance, if lower_included = true and lower = NULL, is that valid? Same with upper.

I’m not seeing any constraint/invariant that says something about those cases. IMO lower/upper_included should imply lower/upper is not NULL.

REFs:

2

DV_INTERVAL inherits the invariants from Interval (BASE/Foundation Types).

3

Hi @thomas.beale I have considered the interval rules (see link above; though I don’t see that case considered. That is why I’m asking :slight_smile:

4

Sorry, read too fast - I thought I read ‘missing invariants’ :wink:

Yes, we should add the following:

lower_included implies lower /= NULL
upper_included implies upper /= NULL

Do you mind adding a PR for this, containing this suggestion?

We will need to process your waiting list of PRs pretty soon :wink:

5

Thanks @thomas.beale rechecking this I believe it should be:

!lower_unbounded <=> lower != NULL
!upper_unbounded <=> upper != NULL

Note the <=> is stronger than the implies because this is an IFF (If and only if - Wikipedia)

Because for intervals that have boundaries the lower/upper should always be there, but the interval could or not include the boundaries, like:

  • [1…10] includes both boundaries in the interval (lower_included = upper_included = true)
  • (1…10] includes only the upper boundary (lower_included = false, upper_included = true)
  • [1…10) includes only the lower boundary (lower_included = true, upper_included = false)
6

You could do this to be strict - the original invariant specification was designed with the sense that if lower_unbounded or upper_unbounded = True, it doesn’t actually matter if any value is attached to lower or upper. The simpler way to state the stricter conditions is:

lower_unbounded xor lower /= Null
upper_unbounded xor upper /= Null
1 Like
7

Makes sense.