Removing from a linked list

Nov 16, 2015 at 8:00 AM
Edited Nov 17, 2015 at 2:13 PM
http://rise4fun.com/Dafny/SrBH

Is it possible to give a Dafny-implementation for the method Remove that satisfies the given contract?

I couldn't find something similar in the test suite.

Thanks in advance
Nov 16, 2015 at 1:01 PM
Perhaps this is interesting:

http://rise4fun.com/Dafny/Xv7
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
http://rise4fun.com/Dafny/SrBH.
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
http://rise4fun.com/Dafny/gplaf
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.