선택 정렬 Dafny

Question

Dafny에서 선택 정렬을 구현하려고합니다.

내 sorted 및 FindMin 기능이 작동하지만 selectionsort 자체에 Dafny가 맞지 않더라도 증명할 수없는 어설 션이 포함되어 있습니다.

predicate sorted(a:array<int>,i:int) 
    requires a != null; 
    requires 0 <= i <= a.Length; 
    reads a; 
{ 
    forall k :: 0 < k < i ==> a[k-1] < a[k] 
} 
method FindMin(a:array<int>,i:int) returns(m:int) 
    requires a != null; 
    requires 0 <= i < a.Length; 
    ensures i <= m < a.Length; 
    ensures forall k :: i <= k < a.Length ==> a[k] >= a[m]; 
{ 
    var j := i; 
    m := i; 
    while(j < a.Length) 
    decreases a.Length - j; 
    invariant i <= j <= a.Length; 
    invariant i <= m < a.Length; 
    invariant forall k :: i <= k < j ==> a[k] >= a[m]; 
    { 
    if(a[j] < a[m]){m := j;} 
    j := j + 1; 
    } 
} 
method selectionsort(a:array<int>) returns(s:array<int>) 
    requires a != null; 
    modifies a; 
    ensures s != null; 
    ensures sorted(s,s.Length); 
{ 
    var c,m := 0,0; 
    var t; 
    s := a; 
    assert s != null; 
    assert s.Length == a.Length; 
    while(c<s.Length) 
    decreases s.Length-c; 
    invariant 0 <= c <= s.Length; 
    invariant c-1 <= m <= s.Length; 
    invariant sorted(s,c); 
    { 
    m := FindMin(s,c); 
    assert forall k :: c <= k < s.Length ==> s[k] >= s[m]; 
    assert forall k :: 0 <= k < c ==> s[k] <= s[m]; 
    assert s[c] >= s[m]; 
    t := s[c]; 
    s[m] := t; 
    s[c] := s[m]; 
    assert s[m] >= s[c]; 
    assert forall k :: c <= k < s.Length ==> s[k] >= s[c]; 
    c := c+1; 
    assert c+1 < s.Length ==> s[c-1] <= s[c]; 
    } 
} 

왜 잘못 : 여기

내 프로그램입니다? "사후 결핍 (postcondtion)"이 의미하는 것은 무엇을 의미합니까? Dafny가 반례를 줄 수 있습니까?

Answer 1

Dafny를 사용하여 프로그램을 확인하는 데 필요한 루프 인바 리언 트의 기본 개념을 이해하는 것 같습니다.

프로그램이 올바르지 않습니다. 이를 발견하는 한 가지 방법은 Visual Studio의 Dafny IDE에서 확인 디버거를 사용하는 것입니다. 마지막으로보고 된 오류 (증가 전의 어설 션은 c)를 클릭하면 배열의 위쪽 절반에 s[c]과 s[m]보다 작은 요소가 포함되어 있음을 알 수 있습니다. 그런 다음 3 문장 스왑 연산을 중심으로 프로그램 포인트를 선택하면 스왑이 실제로 교환되지 않는다는 것을 알 수 있습니다.

스왑을 수정하려면 3- 명령문 스왑의 두 번째 및 세 번째 명령문을 교환하십시오. 더 좋은 방법은, 바로 얻을 코드가 쉽게 Dafny의 다중 할당 문을 사용합니다

두 가지 다른 문제가 있습니다

s[c], s[m] := s[m], s[c]; 

. 한 루프 내의 두번째 주장이 확인되지 않는다는 점이다 : s[m] 어레이의 상부에 작은 요소

assert forall k :: 0 <= k < c ==> s[k] <= s[m]; 

동안 루프 불변 문서화해야한다는 어레이의 하부에있는 소자 선택 정렬 알고리즘의 필수 속성 인 상단 부분의 요소보다 크지 않습니다. 루프는 증가 sorted 엄격 로하는 스와핑하지 않는 한 달성하지 않습니다 정의는 사실에서 줄기를

invariant forall k, l :: 0 <= k < c <= l < a.Length ==> s[k] <= s[l]; 

마지막으로, 속성에 대한 불만이 유지되지 않는 sorted(s,c) 다음 루프 불변 트릭을 수행 배열 요소는 처음에는 모두 별개입니다. 따라서 Dafny는 정렬 루틴에 대한 디자인 결정을 지적합니다. 당신도 당신의 selectionsort 방법은에 전제 조건 (루프 불변의) selectionsort로

forall k, l :: 0 <= k < l < a.Length ==> a[k] != a[l]; 

을 추가하여 단지 당신이없는 중복 요소와 배열에 적용 할 것을 결정할 수 있습니다. 또는 더 일반적으로 sorted의 정의를 수정하여 a[k] > a[m]을 a[k] >= a[m]으로 바꿀 수 있습니다.

코드를 약간 정리하려면 이제 모든 어설 션 문과 선언문을 삭제할 수 있습니다 (t). m은 루프 내에서만 사용되기 때문에 의 선언을 FindMin을 호출하는 명령문으로 이동할 수 있습니다. 그러면 루프 불변 값 c-1 <= m <= s.Length이 필요하지 않음을 알 수 있습니다. 두 개의 decreases 절을 생략 할 수 있습니다. 귀하의 프로그램에 대해, Dafny는 자동으로 이들을 제공합니다.마지막으로, selectionsort 메서드는 주어진 배열을 수정하기 때문에, 참조 a을 out-parameter s에 반환 할 실제 이유가 없습니다. 대신 out 매개 변수를 생략하고 s을 a으로 바꿀 수 있습니다.