Recursion version of Reverse

May 5, 2014 at 6:55 AM
I am trying to prove the correctness of a recursion version of Reverse method based on Test/dafny1/ListContents.dfy but the post-condition cannot be proved.

The implementation is at http://rise4fun.com/Dafny/DTh1

How could I fix these errors?

Thank you very much.
May 8, 2014 at 9:05 PM
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.