Dafny 선형 검색

기본 선형 검색에서 작업 할 때 유효한() 조건 자에 오류가 발생했습니다. 그것은 생성자 및 데이터 메서드에 대한 추가 보장 문을 주석 처리를 제거 할 때만 작동하는 것으로 보입니다. 즉, 내가 내용에 대해 아주 명백 할 때입니다.Dafny 선형 검색

항목을 찾을 수 없을 때 내 검색의 사후 조건에 문제가 있습니다.

이러한 문제를 해결하는 방법에 대한 제안 사항이 있으십니까?

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

출처

2017-11-06 DeirdreCleary

여기서 직각으로 발생하는 몇 가지 문제가 있습니다.

먼저, Dafny가 을 설명하는 Valid의 부분에 대해 추론하기를 꺼 렸음을 알았습니다. 이것은 Dafny의 세트에 대해 추론 할 때 일반적인 문제입니다. 근본적으로, Dafny가 무언가가 set x | 0 <= x < a.Length :: a[x]의 구성원 인 것을 "알"수있는 유일한 방법은 이미 표현식이 a[x] 인 경우 어딘가에있는 것입니다. 추가 후행 조건을 포함하는 해결책은 a[x] 양식의 표현이 많이 포함되어 있기 때문에 효과가 있습니다. 또 다른 해결책 대신 사후의 주장으로 그 사실을 포함하는 것입니다 :

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

둘째, Dafny은 search 절차가 사후 조건을 만족 표시 할 수 없습니다. 검색 진행 상황을 추적하려면 루프 불변성이 필요합니다. 루프 불변량을 디자인하는 방법에 대한 자세한 내용은 guide을 참조하십시오.

셋째, Dafny는 Main에 modifies 절에 관한 문제를보고합니다. constructor에 사후 조건 fresh(a)을 추가하여이 문제를 해결할 수 있습니다. 여기서 문제는 data 메서드가 a을 수정한다고 주장하지만 Dafny는 a이 호출자에게 표시되는지 여부를 알 수 없습니다.

출처

2017-11-06 20:05:50

Dafny 선형 검색

답변

관련 문제