Skip to content

Instantly share code, notes, and snippets.

@jbranchaud
Created March 11, 2013 02:14
Show Gist options
  • Save jbranchaud/5131492 to your computer and use it in GitHub Desktop.
Save jbranchaud/5131492 to your computer and use it in GitHub Desktop.
Exercise 3 from Microsoft's Dafny on Rise4Fun.com
/*
* Keeping the postconditions of Abs the same as above, change
* the body of Abs to just y := x + 2. What precondition do you
* need to annotate the method with in order for the verification
* to go through? What precondition doe you need if the body is
* y := x + 1? What does that precondition say about when you can
* call the method?
*/
method Abs(x: int) returns (y: int)
requires x == -1;
ensures 0 <= y;
ensures 0 <= x ==> x == y;
ensures x < 0 ==> y == -x;
{
y:= x + 2;
}
method Abs2(x: int) returns (y: int)
requires x == -1; // no int value can satisfy this method
ensures 0 <= y;
ensures 0 <= x ==> x == y;
ensures x < 0 ==> y == -x;
{
y:= x + 1;
}
@adamelmohamad
Copy link

Hi, thanks a lot for your solution - I appreciate it. I was just wondering why we have kept the post-conditions related to when x is positive, when the function is not defined for that type of input anyway. It is only defined for negative input. What I am saying is, isn't the line "ensures 0 <= x ==> x == y;" redundant?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment