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

Status

Assignee

Unassigned

Reporter

Rong Chen

Raised By

Rong Chen

Priority

Trivial