Skip to content

Instantly share code, notes, and snippets.

@jbranchaud
Last active December 14, 2015 18:39
Show Gist options
  • Save jbranchaud/5131372 to your computer and use it in GitHub Desktop.
Save jbranchaud/5131372 to your computer and use it in GitHub Desktop.
Exercise 1 from Microsoft's Dafny on Rise4Fun.com
/*
* Write a test method that calls your Max method from
* Exercise 0 and then asserts something about the result.
*/
method Max(a: int, b:int) returns (c: int)
ensures c >= a && c >= b;
ensures a > b ==> c == a;
ensures a <= b ==> c == b;
{
if (a > b) {
return a;
}
else {
return b;
}
}
method Testing() {
var a := 10;
var b := 12;
var v := Max(a, b);
assert v >= a && v >= b;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment