Dafny 카운트를 증명하는 방법 <size

Question

나는 현재 Dafny를 배우고 있습니다. 나는 완전히 보조 정리에 익숙해 져 있고 그것을 사용하는 방법을 모른다. 튜토리얼은 도움이되지 않습니다. 내가 증명하고 싶다면 count(a) <= |a| 어떻게해야합니까? 도와 줘서 고맙다.

function count(a: seq<bool>): nat 
ensures count(a) <= |a|; 
{ 
    if |a| == 0 then 0 else 
    (if a[0] then 1 else 0) + count(a[1..]) 
} 

Answer 1

당신은 이미 그것을 증명했습니다! 당신은 함수의 사후 조건으로 당신이 원하는 속성을 썼고 Dafny는 불평없이 그것을 확인합니다. 그게 전부 야.

또한 보조 정리를 사용하여 속성을 증명할 수도 있습니다. 다음 예는 다음과 같습니다

function count(a: seq<bool>): nat 
{ 
    if |a| == 0 then 0 else 
    (if a[0] then 1 else 0) + count(a[1..]) 
} 

lemma CountProperty(a: seq<bool>) 
    ensures count(a) <= |a| 
{ 
} 

을 다시 말하지만, 당신이 그것을 증명했다, 그래서 Dafny는 불만을 발행하지 않고 보조 정리를 확인!

Dafny가 항상 자동으로 물건을 증명한다고 가정하는 것은 정확하지 않습니다. 따라서 증명을 수동으로 작성하는 방법을 배우는 것도 좋은 생각입니다. 이 속성에 대한 수동 증거가 있습니다. 이 같은 증거를 작성

lemma {:induction false} CountProperty(a: seq<bool>) 
    ensures count(a) <= |a| 
{ 
    // Let's consider two cases, just like the definition of "count" 
    // considers two cases. 
    if |a| == 0 { 
    // In this case, we have: 
    assert count(a) == 0 && |a| == 0; 
    // so the postcondition follows easily. 
    } else { 
    // By the definition of "count", we have: 
    assert count(a) == (if a[0] then 1 else 0) + count(a[1..]); 
    // We know an upper bound on the first term of the addition: 
    assert (if a[0] then 1 else 0) <= 1; 
    // We can also obtain an upper bound on the second term by 
    // calling the lemma recursively. We do that here: 
    CountProperty(a[1..]); 
    // The call we just did gives us the following property: 
    assert count(a[1..]) <= |a[1..]|; 
    // Putting these two upper bounds together, we have: 
    assert count(a) <= 1 + |a[1..]|; 
    // We're almost done. We just need to relate |a[1..]| to |a|. 
    // This is easy: 
    assert |a[1..]| == |a| - 1; 
    // By the last two assertions, we now have: 
    assert count(a) <= 1 + |a| - 1; 
    // which is the postcondition we have to prove. 
    } 
} 

더 좋은 방법 : 그냥 확인 Dafny 자동 유도을하려고하지 않습니다 만들기 위해, 나는 (따라서 일반적으로 Dafny보다 더 열심히 우리의 삶을 것이다 만들기)을 해제하는 지시어를 사용

lemma {:induction false} CountProperty(a: seq<bool>) 
    ensures count(a) <= |a| 
{ 
    if |a| == 0 { 
    // trivial 
    } else { 
    calc { 
     count(a); 
    == // def. count 
     (if a[0] then 1 else 0) + count(a[1..]); 
    <= // left term is bounded by 1 
     1 + count(a[1..]); 
    <= { CountProperty(a[1..]); } // induction hypothesis gives a bound for the right term 
     1 + |a[1..]|; 
    == { assert |a[1..]| == |a| - 1; } 
     |a|; 
    } 
    } 
} 

나는 이것이 당신이 시작 얻을 수 있기를 바랍니다 : Dafny "는 CALC 문"을 호출하는 검증 계산을 사용하는 것입니다.

프로그램 안전하게

RUSTAN