Dafny에서 두 정수를 불변량으로 곱하는 간단한 방법

Question

이 Q3 메서드는 res | n0 |에 m0을 추가하여 n0 * m0을 통근합니다. 타임스. n0이 음수이면 n0 * m0 = -n0 * -m0으로 n0와 m0을 모두 반전시킵니다.

문제는 불변량이 부울 유형 일 필요가 있기 때문에 내 불변성이 어떻게 보이는지 정확히 알지 못한다는 것입니다. 아무도 불변 부울 조건이 어떻게 생겼는지 말해 줄 수 있습니까? 내가 Abs((n0)-n)*m == res에 대해 생각했지만 그게 작동하지 않습니다.

method Q3(n0 : int, m0 : int) returns (res : int) 
    ensures n0*m0 == res 
{ 

    var n, m : int; 
    res := 0; 
    if (n0 >= 0) 
    {n,m := n0, m0;} 
    else 
    {n,m := -n0, -m0;} 

    while (0 < n) 
    invariant Abs((n0)-n)*m 
    { 
    res := res + m; 
    n := n - 1; 
    } 
} 

function Abs(x: int): int 
{ 
    if x < 0 then -x else x 
} 

Answer 1

루프 불변성을 디자인 할 때는 먼저 거꾸로 작업하는 것이 좋습니다. 루프 종료 후 무엇을 알아야합니까?

이 방법의 경우 루프가 종료되면 n0 * m0 == res의 사후 조건을 설정해야하므로 루프 불변량의 시작 지점이됩니다.

res은 루프에 의해 변경되므로 n0 * m0 == res은 그 자체가 불변하지 않습니다. 대신 루프가 어떻게이 목표를 향해 "진전"을하는지 생각해야합니다. 이 루프는 m을 res에 추가하여 진행하므로 총계는 n 회입니다. n이 0이면 루프가 종료됩니다.

일반적인 패턴이 유용합니다. invariant는 "지금까지"수행 된 작업과 "할 일"이 무엇인지에 대해 이야기해야합니다. 이 경우 지금까지 수행 된 작업은 res이며 남은 작업은 나머지 n 개가 m입니다. 루프를 반복 할 때마다 수행해야 할 작업이 하나씩 필요하며이를 수행하여 불변성을 유지합니다.

즉,이 루프의 올바른 불변 값은 res + n * m == n0 * m0입니다.

또한 Dafny Tutorial에는 유용 ​​할 수도있는 루프 불변성에 관한 섹션이 있습니다.