This is a partial solution to problem 2 in Dafny.
Task 1: Dafny checks termination of the implementation.
Task 2a: The property is added as a postcondition to the refine method.
Task 2b: The predicates necessary for the verification have been defined and are checked by Dafny to be well-formed. An informal proof sketch is added as a comment. The necessary specification is added to the implementation but commented out, as the verification with Dafny fails.