einfache Methode Nachbedingung könnte nicht halten

Question

Ich habe Probleme mit dieser einfachen Methode in Dafny und ich weiß nicht, warum es nicht funktioniert. Da es keinen Debugger gibt und ich neu in dieser Sprache bin, hoffe ich, dass jemand helfen kann. Ich denke, die Spezifikation unvollständig ist ..

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

Als ich es in dem Microsoft-dafny Compiler laufen bekomme ich folgend:

Eine Nachbedingung möglicherweise nicht auf diesem Rückpfad halten. (Zeile 8) Dies ist die Nachbedingung, die möglicherweise nicht gilt. (Linie 2)

Answer 1

Das Problem ist, dass x und y gleich sein könnten, wobei in diesem Fall big und small werden auch gleich sein.

Sie können die Nachbedingung korrigieren, indem Sie sie in big >= small ändern. Oder Sie möchten dem Anrufer verbieten, immer die gleichen x und y zu übergeben, können Sie eine Vorbedingung hinzufügen, die x != y erfordert.