Dafny lineare Suche

Question

Bei der Arbeit an einer grundlegenden linearen Suche habe ich einen Fehler mit meinem Prädikat Valid() festgestellt. Es scheint nur zu funktionieren, wenn ich die zusätzlichen Anweisungen für den Konstruktor und die Datenmethode auskommentiere. Das heißt, wenn ich über den Inhalt sehr explizit bin.

Ich habe auch Probleme mit der Nachbedingung meiner Suche, wenn das Element nicht gefunden wird.

Haben Sie Vorschläge, wie Sie diese beheben können?

class Search{ 
    ghost var Contents: set<int>; 
    var a : array<int>; 

    predicate Valid() 
     reads this, a; 
    { 
     a != null && 
     a.Length > 0 && 

     Contents == set x | 0 <= x < a.Length :: a[x] 
    } 

    constructor() 
     ensures a != null; 
     ensures a.Length == 4; 
     //ensures a[0] == 0; 
     ensures Valid(); 
    { 
     a := new int[4](_ => 0); 
     Contents := {0}; 
     new; 
    } 

    method data() 
     modifies this, a; 
     requires Valid(); 
     requires a != null; 
     requires a.Length == 4; 
     ensures a != null; 
     ensures a.Length == 4; 
     // ensures a[0] == 0; 
     // ensures a[1] == 1; 
     // ensures a[2] == 2; 
     // ensures a[3] == 3; 
     ensures Valid(); 
    { 
     a[0] := 0; 
     a[1] := 1; 
     a[2] := 2; 
     a[3] := 3; 
     Contents := {0, 1, 2, 3}; 
    } 

    method search(e: int) returns (r: bool) 
     modifies this, a; 
     requires Valid(); 
     ensures Valid(); 
     ensures r == (e in Contents) 
     ensures r == exists i: int :: 0 <= i < a.Length && a[i] == e 
    { 
     var length := a.Length - 1; 

     while (length >= 0) 
      decreases length; 
     { 
      var removed := a[length]; 
      if (e == removed) 
      { 
       return true; 
      } 
      length := length - 1; 
     } 
     return false; 
    } 
    } 


method Main() 
{ 
    var s := new Search(); 
    s.data(); 
} 

Answer 1

Hier gibt es mehrere orthogonale Probleme.

Zuerst haben Sie bemerkt, dass Dafny nur widerwillig über den Teil Valid spricht, der Contents beschreibt. Dies ist ein häufiges Problem beim Nachdenken über Sets in Dafny. Im Wesentlichen wird die einzige Möglichkeit, Dafny jemals "bemerken", dass etwas ein Mitglied der Menge ist set x | 0 <= x < a.Length :: a[x] ist, wenn es bereits den Ausdruck a[x] irgendwo herumliegen hat. Ihre Lösung, zusätzliche Nachbedingungen einzubeziehen, funktioniert, weil sie viele Ausdrücke des Formulars a[x] erwähnt. Eine andere Lösung ist es, diese Fakten als Behauptungen statt Nachbedingungen enthalten:

// in data() 
assert a[0] == 0; 
assert a[1] == 1; 
assert a[2] == 2; 
assert a[3] == 3; 

Zweitens Dafny kann nicht zeigen Sie Ihre search Verfahren seine Nachbedingung erfüllt. Sie benötigen eine Schleifeninvariante, um den Fortschritt der Suche zu verfolgen. Weitere Informationen zum Entwerfen von Schleifeninvarianten finden Sie unter guide.

Drittens meldet Dafny ein Problem mit Ihrer Main über Änderungen Klauseln. Sie können das beheben, indem Sie eine Nachbedingung fresh(a) zu der constructor hinzufügen. Das Problem hier ist, dass die data Methode behauptet, a zu ändern, aber Dafny kann nicht feststellen, ob a von dem Aufrufer sichtbar ist.