From: Uwe S. <us...@on...> - 2001-12-14 05:44:13
|
Hi, as you may know, I am currently rebuilding the elj database access classes as descendents of the GOBO classes DS_BILINEAR and DS_BILINEAR_CURSOR. I'm having a little trouble with the postconditions definition: Result implies (cursor_item (a_cursor) = first) of DS_LINEAR.cursor_is_first and definition: Result implies (cursor_item (a_cursor) = last) of DS_BILINEAR.cursor_is_last Wouldn't it be better to define both as same_items (cursor_item (a_cursor), first) and same_items (cursor_item (a_cursor), last) ? DS_LINEAR inherits DS_SEARCHABLE and I think it would be more consistent to make every comparison use the same algorithm. Regards Uwe |