DTV12 — DTV Issue: Error in CLIF definition of consecutive sequence

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.

Accept the text correction