Formal Specification

Using Dafny language answer the following questions

Question 1: Write a method Max that takes two integer parameters and returns their maximum. Add appropriate annotations and make sure your code verifies.

Question 2: Write a test method that calls your Max method from Exercise 1 and then asserts something about the result.

Formal Specification Homework 3 10 Marks Using Dafny language answer the following questions Question 1: Write a method Max that takes two integer parameters and returns their maximum. Add appropriate annotations and make sure your code verifies. method Max(a: int, b: int) returns (c: int) // What postcondition should go here, so that the function operates as expected? // Hint: there are many ways to write this. { // fill in the code here } Question 2: Write a test method that calls your Max method from Exercise 1 and then asserts something about the result. method Max(a: int, b:int) returns (c: int) // Use your code from Exercise 0 method Testing() { // Assert some things about Max. Does it operate as you expect? // If it does not, can you think of a way to fix it? }