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 at 3:03 PM

superseded by

Thomas Beale July 24, 2008 at 3:03 PM

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

Duplicate

Details

Assignee

Reporter

Raised By

Rong Chen

Priority

Created May 16, 2008 at 8:03 PM
Updated July 30, 2008 at 2:40 PM
Resolved July 30, 2008 at 2:40 PM