Dafny를 사용한 자동 프로그램 검증

프로그램 검증

Program Verification is the process of proving that the program does exactly what the developer intended it to do and noting more.

기본적으로 다음과 같은 것을 만들지 않도록 방지할 수 있습니다.

정확히는 아니지만 충분히 가깝습니다.

테스트가 충분하지 않은 이유

“Testing shows the presence, not the absence of bugs”

-Edsgar W. Dijkstra

이 게시물에서 HAL은 슈퍼 스마트 AI가 아니라 산술 연산을 수행하는 간단한 프로그램입니다.
HAL을 테스트한다면 그는 질문에 대한 올바른 결과를 제공할 만큼 충분히 똑똑합니다.

Hal what is 2 + 2?
HAL: 4
HAL what is 2*2 ?
HAL: 4

HAL은 테스트에서 질문에 대한 정답을 제공합니다. 이는 HAL이 의도한 대로 작동한다는 것을 의미합니다.

스포일러 경고
아니

HAL은 우리가 그것을 실행할 때마다 2를 반환할 수 있으며 우리는 그러한 테스트로 그것을 알아차리지 못합니다. 실생활에서 아무도 프로그램에 이러한 작은 테스트를 사용하지 않을 것이지만 철저한 테스트를 수행하더라도 프로그램이 작동할 것이라고 100% 확신할 수는 없습니다.

그래서 해결책은 무엇입니까?

Formal Methods

형식적 방법은 프로그램 검증에 수학을 사용하는 멋진 방법입니다.



공식적인 방법은 수행하기 정말 어렵고 이 기사는 이에 대한 정확한 내용이 아니므로 바로 요점으로 들어가겠습니다. 그러나 우리를 위해 공식적인 검증을 수행하는 프로그램은 우리가 작성하는 코드와 이를 검증하기 위해 코드가 수행해야 하는 작업을 취한다는 점을 기억하십시오.

다프니

Dafny is programming language that helps us in doing formal verification

dafny는 C#에 가깝기 때문에 dafny와 많은 부분이 비슷합니다.

Dafny의 가장 멋진 점은 코드를 작성하는 동안 실수를 하고 있음을 보여줄 수 있다는 것입니다.

예:

method Double(x: int) returns (r: int)
   requires  x > 0
   ensures r==2*x
{
   r := x + x;
}

위의 코드에는 받는 int의 double 값을 반환하는 Double 메서드가 있습니다.
키워드를 사용하면 코드가 수행해야 할 작업을 지정할 수 있습니다.
바보 같은 실수를 해서 + 대신에 - dafny가 오류를 보여줄 것입니다.



Dafny는 이 모든 것을 학습할 수 있는 정말 좋은 가이드를 제공하며Best Guide 아래에서 내가 배운 내용을 요약할 것입니다.

내가 배운 것의 요약

장점

코드를 작성하는 동안 버그를 감지할 수 있습니다.

C#과 유사하며 VS code extension으로 설치할 수 있습니다.

훌륭한 학습 기회를 제공합니다.

단점

Dafny는 Boogie Intermediate 언어와 Z3 SMT 솔버를 사용하므로 둘 다 할 수 있는 작업이 제한됩니다.

기존 코드에 Dafny를 사용할 수 없습니다. dafny를 사용하려면 새 코드를 작성해야 합니다.

Dafny의 다른 부분

방법

메서드는 0개 이상의 인수를 취하고 0개 이상의 값을 반환하는 함수입니다. 그것은 dafny 내부에 존재하는 기능과 다릅니다. dafny의 주요 메소드는 Main()
확인에는 필요하지 않지만 여기에서 코드 실행이 시작되므로 코드에서 .net 실행 파일을 가져오는 데 필요합니다.

 method Main()
 {

   print "Hello World";
   print "\n";
 }

기능

키워드 function은 dafny의 순수 함수에 사용됩니다. 그들은 프로그램의 상태를 변경할 수 없으며 컴파일된 코드에 나타나지 않기 때문에 기본적으로 유령입니다. 수학적 논리를 정의하는 데 사용됩니다.
예:

function fib(n: nat): nat
{
    if n < 2 then  n
    else
        fib(n - 1) + fib(n - 2)
}

사전 및 사후 조건

그들은 프로그램의 사양을 지정하는 데 도움이 됩니다. 사전 조건은 메소드 실행 전에 참이어야 하고 사후 조건은 프로그램 실행 후에 참이어야 합니다.

루프 불변

그들은 루프 조건의 범위를 지정합니다. 루프 i가 0에서 n으로 간다고 가정하면 루프 불변량을 다음과 같이 지정할 수 있습니다.

while i<n
   invariant 1 <= i <=n
   {
      i := i + 1;
   }
   assert i == n; 

루프가 몇 번 발생하는지 이해하는 데 도움이 됩니다.

종료

Dafny는 루프가 종료되는지 여부를 자동으로 결정할 수 있습니다.

while i<n
       invariant 1 <= i <=n
   {
      i := i + 1; 
       if i<n  {i:= 1;}
       if i==1 {break;}
   }

이 코드를 실행하면 dafny는 코드가 종료된다는 것을 알 수 있습니다.

Dafny를 사용한 피보나치 검증

function fib(n: nat): nat
decreases n
{
    if n < 2 then  n
    else
        fib(n - 1) + fib(n - 2)
}


method ComputeFib(n: nat) returns (b: nat)
    ensures b == fib(n)  
{
    if n == 0 { return 0; }
    var i: int := 1;
    var c := 1;
        b := 1 ;
    while i < n
        invariant  0< i <= n
        invariant b == fib(i)
        invariant c == fib(i + 1)
    {
        b, c := c, b + c;
        i := i + 1;
    }
}


 method Main()
 {
   var result:int := ComputeFib(6);
   print "fib(6):= ";
   print result;
   print "\n";
 }