
Key: DTV12113

Legacy Issue Number: 19459

Status: closed

Source: Thematix Partners LLC ( Mr. Edward J. Barkmeyer)

Summary:
Spec: DTV
Version: 1.0 and 1.1
Source: Ed Barkmeyer, NIST
Summary:
In Annex D.2.4 of DTV, the CLIF Definition of ‘consecutive sequence’ is:
(forall (s) (iff ("consecutive sequence" s)(and
(sequence s)
(forall (sp1)
(if
(and
("sequence has sequence position" s sp1)
(exists (sp2)
("next sequence position succeeds sequence position" sp2 sp1)) )
(forall (x1 x2)
(if
(and
("sequence position has index" sp1 x1)
("sequence position has index" sp2 x2))
(= x2 (+ x1 1)) ))
)) )))
This is clearly incorrect. The scope of the quantification “exists (sp2)” ends with the right paren before “(forall (x1 x2))”. So the last occurrence of sp2 is not associated with the quantified variable.
The correct formulation is:
(forall (s) (iff ("consecutive sequence" s)
(and
(sequence s)
(forall (sp1 sp2 x1 x2)
(if
(and
("sequence has sequence position" s sp1)
("next sequence position succeeds sequence position" sp2 sp1)
("sequence position has index" sp1 x1)
("sequence position has index" sp2 x2))
(= x2 (+ x1 1)) ))
)))
The English definitions might also be improved by adding a Description:
A consecutive sequence is a sequence in which consecutive sequence positions have consecutive indices.

Reported: DTV 1.0 — Wed, 11 Jun 2014 04:00 GMT

Disposition: Resolved — DTV 1.2

Disposition Summary:
Accept the text correction

Updated: Wed, 8 Jul 2015 11:40 GMT
DTV12 — DTV Issue: Error in CLIF definition of consecutive sequence
 Key: DTV12113
 OMG Task Force: DateTime Vocabulary (DTV) 1.2 RTF