Upper limit of row index needs to be inclusive for ith_row of ITEM_TABLE

Description

CURRENT:
ith_row(i:Integer): CLUSTER
require
i >0 and i < row_count

The upper limit needs to inclusive to get the last row. The lower limit could be improved as "i >= 1" to be consistent with other invariants

Activity

Show:
Thomas Beale
July 24, 2008, 3:03 PM

Accept prior to rejecting as obsolete (superseded by SPEC-271)

Thomas Beale
July 24, 2008, 3:03 PM

superseded by

Assignee

Unassigned

Reporter

Rong Chen

Raised By

Rong Chen

Priority

Trivial
Configure