IncreMentally Challenged: Problem 4

· Uncategorized
Author

This is a complete solution to problem 4 in Dafny.

Task 1 is implemented in the method Node.Copy. Requirements are verified as follows:

  1. Dafny checks absence of runtime errors.
  2. Dafny checks termination.
  3. Postcondition (b) of Copy.
  4. Since Copy has an empty modifies clause (default), Dafny check the absence of side effects.
  5. Postconditions (a), (c) and (d) of Copy.

Task 2 is implemented in methods Node.Eval and Node.EvalCopy. REquirements are verified as follows:

  1. Dafny checks absence of runtime errors.
  2. Dafny checks termination.
  3. Postcondition of Eval.
  4. Assert at the end of EvalCopy.

 

problem4

Leave a Comment