Nov 17, 2015 at 9:15 AM
Edited Nov 17, 2015 at 2:16 PM
Yes, of course this example is very interesting. I knew it.
The problem is that the fact expressed by the comment
" // not allowed to remove end nodes; you may think of them as a sentinel nodes"
clashes (I guess) with the contract of the method Remove I proposed in
I mean, the implementation of Remove requires to possibly change the first node, and I haven't find the way to do it properly.
Moreover, in the program in
I consider the head of the list as a sentinel, but Dafny is not able to verify the (commented) postcondition Valid(). Why?
I think the result is obviously a valid linked list.