Skip to content

Instantly share code, notes, and snippets.

@jbranchaud
Created March 12, 2013 14:40
Show Gist options
  • Save jbranchaud/5143424 to your computer and use it in GitHub Desktop.
Save jbranchaud/5143424 to your computer and use it in GitHub Desktop.
Exercise 5 from Microsoft's Dafny on Rise4Fun.com
/*
* Change your test method from Exercise 4 to capture the value
* of max to a variable, and then do the checks from Exercise 4
* using the variable. Dafny will reject this program because you
* are calling max from real code. Fix this problem using a
* function method.
*/
function method max(a: int, b: int): int
{
if a > b then a else b
}
method Testing() {
// Add assertions to check max here. Be sure to capture it to a local variable
var v := max(10,12);
assert(v == 12);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment