постусловие простого метода может не выполняться

У меня проблемы с этим простым методом в Дафни, и я не знаю, почему он не работает. Поскольку отладчика нет, а я новичок в этом языке, надеюсь, кто-нибудь сможет помочь. Я думаю, что спецификация неполная ..

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;}
}

Когда я запускаю его в компиляторе Microsoft dafny, я получаю следующее:

Постусловие может не выполняться на этом пути возврата. (Строка 8) Это постусловие, которое может не выполняться. (строка 2)


methods dafny
person NewbieJava    schedule 04.12.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Проблема в том, что x и y могут быть равны, и в этом случае big и small также будут равны.

Вы можете исправить постусловие, изменив его на big >= small. Или, если вы хотите запретить вызывающей стороне когда-либо передавать равные x и y, вы можете добавить предварительное условие, требующее, чтобы x != y.

person James Wilcox    schedule 04.12.2017