Dafny 메서드가 반전 된 문자 배열을 반환합니다.

Question

문자의 입력 배열을 취하고 입력 배열로 구성된 다른 배열을 역순으로 출력하는 메서드를 구현하고 싶습니다. 1 개 인덱스 범위를 6에서

predicate reversed (arr : array<char>, outarr: array<char>) 
requires arr != null && outarr != null 
//requires 0<=k<=arr.Length-1 
reads arr, outarr 
{ 
    forall k :: 0<=k<=arr.Length-1 ==> outarr[k] == arr[(arr.Length-1-k)] 
} 

method yarra(arr : array<char>) returns (outarr : array<char>) 
requires arr != null && arr.Length > 0 
ensures outarr != null && reversed(arr,outarr) 
{ 
    var i:= 0; 
    var j:= arr.Length-1; 
    outarr := new char[arr.Length]; 
    outarr[0] := arr[j]; 
    i := i+1; 
    j := j-1; 
    while i<arr.Length && 0<=j<arr.Length 
    invariant 0<=i<=arr.Length 
    decreases arr.Length-i, j 
    { 
    outarr[i] := arr[j]; 
    i:=i+1; 
    j:=j-1; 
    } 
    //return outarr; 
} 

method Main() 
{ 
    var s := ['a','b','a','b','a','b','a','b','a','b','a','b']; 
    var a,b,c,d := new char[5], new char[5], new char[5], new char[5]; 
    a[0], a[1], a[2], a[3], a[4] := 'y', 'a', 'r', 'r', 'a'; 
    d[0], d[1], d[2], d[3], d[4] := 'y', 'a', 'r', 'r', 'a'; 
    b := yarra(a); 
    c := yarra(b); 
    assert c[..] == a[..]; 
    //assert c.Length > -2; 
    //assert d[0] == a[0]; 
    //print c; print a; 
} 

1. 오류 : 내 코드하지만 오류 "우리의 범위의 인덱스"내가 여기

   일이 무엇인지 전혀 모르는 을 "후 상태가 유지되지 않을 수도 있습니다"가지고있다 43

2. 오류 2이 리턴 경로에 사후 조건이 적용되지 않을 수 있습니다. 21 2

3. 이것은 보유 할 수없는 사후 조건입니다. (13) (26)

   stdin.dfy (6,43) : 오류 : 인덱스 범위를 벗어
   stdin.dfy (21,2) : 오류 BP5003 : 사후 조건이 반환 경로에 개최하지 않을 수 있습니다.
   stdin.dfy (13,26) : 관련 위치 : 이것은 보유 할 수없는 사후 조건입니다.
   stdin.dfy (6,2) : 관련 위치
   stdin.dfy (6,47) : 관련 위치

Answer 1

Here은 검증 프로그램의 버전입니다.

수정해야 할 몇 가지 문제가있었습니다.

먼저 Dafny가 outarr[k]이 범위 내에 있다는 것을 알 수 없으므로 reversed이라는 정의가 잘못 작성되었습니다. 전제 조건 arr.Length == outarr.Length을 reversed에 추가하여이 문제를 해결했습니다.

다음으로,이 새로운 전제 조건은 reversed이 호출 된 곳이면 어디서나 고려되어야합니다. 그러한 장소는 yarra의 사후 조건에 있습니다.이 사후 조건은 추가 사후 조건 arr.Length == outarr.Length을 추가하여 수정했습니다.

그러면 Dafny는 reversed에 대한 사후 조건이 yarra에 없을 수 있다고 불평합니다. 이를 위해서는 루프 불변성을 강화해야합니다. 이것은 각 인덱스에 대해 하나씩 배열함으로써 배열의 모든 인덱스에 대해 뭔가를 증명하려고 시도하는 전형적인 경우입니다. 이러한 상황에서 올바른 루프 불변량은 "현재 인덱스보다 작은 모든 인덱스에서이를 확립했습니다."입니다. 올바른 불변 그래서 우리는이 루프에서 구축하고있는 것은, 그 outarr[k] == arr[arr.Length-1-k]입니다 :이 통과하는

forall k | 0 <= k < i :: outarr[k] == arr[arr.Length-1-k] 

마지막으로, 우리는 불변 j == arr.Length - 1 - i이 필요합니다. (사실,이 불변량은 우리가 j을 완전히 제거 할 수 있음을 암시하지만, 그렇게하지는 않았다.)