CODEWITHSUNDEEP
methodsdafny
NewbieJava
NewbieJava

Reputation: 117

simple method postcondition might not hold

I'm having problems with this simple method in Dafny and I don't know why it doesn't work. Since there are no debugger and I'm new to this language I hope somebody can help. I think the specification is incomplete..

method Q2(x : int, y : int) returns (big : int, small : int) 
  ensures big > small;
{
  if (x > y)
    {big, small := x, y;}
  else
    {big, small := y, x;}
}

When I run it in the microsoft dafny compiler I get the following:

A postcondition might not hold on this return path. (Line 8) This is the postcondition that might not hold. (Line 2)

Upvotes: 2

Views: 819

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

The issue is that x and y might be equal, in which case, big and small will also be equal.

You can fix the postcondition by changing it to big >= small. Or, you want to forbid the caller from ever passing equal x and y, you could add a precondition requiring that x != y.

Upvotes: 1

Related Questions