linked-list - How to travse a linked list in my postcodition use across loop in Eiffel?

Question

I try to use across 1|..|list.count as j all list.i_th(z) ~ old list.i_th(z) end

but it says unknown identifier z. Whats wrong with this syntax??

Answer 1

The syntax is correct. However, no identifier of name z is declared, hence the error. There is a cursor variable j instead. The items at the current cursor position are accessed with j.item.

Another issue is that j is evaluated in the current context (the postcondition), but old expressions are evaluated before the feature body is executed, where j is absent. As a result the code with old list.i_th (j.item) would not compile. In other words, the value should be taken from the old list but with the current index. The expression (old list).i_th (j.item) does the trick.

But this still does not do what is needed. It turns out that old list = list because the reference to the list object remains the same. To get the old elements, the copy of the list is required instead: (old list.twin).

Combining all the above, the expression should look like across 1 |..| list.count as j all list.i_th (j.item) ~ (old list.twin).i_th (j.item) end.