indexing
description: "Sets of compactly coded date-time pairs"
date: "$Date$"
revision: "$Revision$"
class interface
DATE_TIME_SET
create
make (n: INTEGER)
n
require
positive: n > 0
feature
item (i: INTEGER): DATE_TIME
i
require
index_in_range: 1 <= i and i <= last
last: INTEGER
feature
put (dt: DATE_TIME)
dt
require
exists: dt /= void
ensure
inserted_date: equal (date_set.item (last), dt.date)
inserted_time: equal (time_set.item (last), dt.time)
feature
make (n: INTEGER)
n
require
positive: n > 0
invariant
last_non_negative: last >= 0
last1: last = date_set.last
last2: last = time_set.last
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- DATE_TIME_SET