Problem 2

Reverse a linked list (extension from Exercise 6, Problem 4).

Classes:

ReversibleLinkedList([values])

Extend a LinkedList with reverse operation.

class ReversibleLinkedList(values: Optional[Iterable[int]] = None)

Extend a LinkedList with reverse operation.

Establishes

• len(list(self.values())) == self.count()

• self._last is not None ⇒ self._last.next_node is None

• len(list(self.values())) != 0 ^ self.is_empty()

• self.is_empty() ^ (self._first is not None and self._last is not None)

Methods:

reverse()	Reverse the elements of the list.
__eq__(value, /)	Return self==value.
__ge__(value, /)	Return self>=value.
__gt__(value, /)	Return self>value.
__init__([values])	Initialize the list by populating it with the given values.
__le__(value, /)	Return self<=value.
__lt__(value, /)	Return self<value.
__ne__(value, /)	Return self!=value.
__str__()	Return str(self).
add_first(value)	Prepend the value to the list.
add_last(value)	Append the value to the list.
clear()	Remove all elements in the list.
count()
cursor()	Get a cursor pointing to the beginning of the list.
get(index)	Retrieve the index-th element of the list.
is_empty()
remove_first()	Remove first element of the list.
remove_last()	Remove the last element of the list.
set(index, value)	Set the index-th element to value.
values()	Iterate over all the values in the list.

Attributes:

__invariants__

reverse() → None

Reverse the elements of the list.

OLD

• .count = self.count()

• .values = list(self.values())

Ensures

• self.count() == OLD.count

• list(self.values()) == list(reversed(OLD.values))

__eq__(value, /)

Return self==value.

__ge__(value, /)

Return self>=value.

__gt__(value, /)

Return self>value.

__init__(values: Optional[Iterable[int]] = None) → None

Initialize the list by populating it with the given values.

__invariants__ = [<icontract._types.Contract object>, <icontract._types.Contract object>, <icontract._types.Contract object>, <icontract._types.Contract object>]

__le__(value, /)

Return self<=value.

__lt__(value, /)

Return self<value.

__ne__(value, /)

Return self!=value.

__str__()

Return str(self).

add_first(value: int) → None

Prepend the value to the list.

OLD

• .values = list(self.values())

• .count = self.count()

Ensures

• self.count() == OLD.count + 1

• not self.is_empty()

• [value] + OLD.values == list(self.values())

add_last(value: int) → None

Append the value to the list.

OLD

• .values = list(self.values())

• .count = self.count()

Ensures

• self.count() == OLD.count + 1

• not self.is_empty()

• OLD.values + [value] == list(self.values())

clear() → None

Remove all elements in the list.

Requires

• not self.is_empty()

Ensures

• self.count() == 0

• self.is_empty()

count() → int

cursor() → Cursor

Get a cursor pointing to the beginning of the list.

get(index: int) → int

Retrieve the index-th element of the list.

Requires

• 0 <= index < self.count()

Ensures

• list(self.values())[index] == result

is_empty() → bool

remove_first() → int

Remove first element of the list.

Requires

• not self.is_empty()

OLD

• .count = self.count()

• .values = list(self.values())

Ensures

• OLD.values[0] == result

• self.count() == OLD.count - 1

• OLD.values[1:] == list(self.values())

remove_last() → int

Remove the last element of the list.

Requires

• not self.is_empty()

OLD

• .values = list(self.values())

• .count = self.count()

Ensures

• OLD.values[-1] == result

• self.count() == OLD.count - 1

• OLD.values[:-1] == list(self.values())

set(index: int, value: int) → None

Set the index-th element to value.

Requires

• 0 <= index < self.count()

Ensures

• list(self.values())[index] == value

values() → Iterator[int]

Iterate over all the values in the list.