IncreMentally Challenged: Problem 2

· Uncategorized

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.


Leave a Comment