/// require: true; возвращает число элементов списка; /// count in[0,n] /// (count == 0) eqviv empty(); /// index: require: not empty(); возвращает индекс /// активного элемента. /// search_res: require: true; возвращает true, /// если последний поиск был успешным. /// Команды: /// put_left(elem): require: true; /// ensure: добавить новый элемент (elem) слева от курсора; /// put_right(elem): require: true; /// ensure: добавить новый элемент (elem) справа от /// курсора; /// remove: require: not empty(); /// ensure: удалить активный элемент; /// особо обрабатывается удаление последнего и /// единственного элементов /// операции с курсором: /// start: require: true; /// ensure: сделать активным первый элемент; /// finish: require: true; /// ensure: сделать активным последний элемент; /// go_prev: require: not (index = 1); /// ensure: сделать активным предыдущий элемент; |