(b) Given the following Dafny program, where you may assume that the contract provided is correct,...

 

Transcribed Image Text:

(b) Given the following Dafny program, where you may assume that the contract provided is correct, I. identify at least two errors in the code II. provide an appropriate loop invariant III. provide an appropriate loop variant method M (x: int, y: int) returns (r: int) requires y <0; ensures r == x + y; { r = 0; var n := y; { } while (n != 0) r n = r 1; = n + 2; - Explain your solution in each case. [6 marks] (b) Given the following Dafny program, where you may assume that the contract provided is correct, I. identify at least two errors in the code II. provide an appropriate loop invariant III. provide an appropriate loop variant method M (x: int, y: int) returns (r: int) requires y <0; ensures r == x + y; { r = 0; var n := y; { } while (n != 0) r n = r 1; = n + 2; - Explain your solution in each case. [6 marks]