
I am trying to prove the correctness of a recursion version of Reverse method based on Test/dafny1/ListContents.dfy but the postcondition cannot be proved.
The implementation is at
http://rise4fun.com/Dafny/DTh1
How could I fix these errors?
Thank you very much.



I believe that ghost variables also need to be updated.
This would also mean that if after the recursive call, the returned object is Valid(), then appending a node with the current implementation would not preserve validity. You would need to cascade the new node and its data to update the footprint and list of
the previous ones.

