Dafny

Dafny

패러다임	명령형, 함수형
설계자	K. 루스탄 M. 레이노
개발자	마이크로소프트 리서치
발표일	2009년(17년 전)(2009)
최근 버전	4.11.0
최근 버전 출시일	2025년 8월 25일(14개월 전)(2025-08-25)
자료형 체계	정적, 강하고 안전함
라이선스	MIT
파일 확장자	.dfy
웹사이트	dafny.org

Dafny는 C#, 자바, 자바스크립트, Go, 파이썬과 같은 다른 프로그래밍 언어로 컴파일되는 명령형 및 함수형 컴파일 언어이다. 이 언어는 사전 조건, 사후 조건, 루프 불변성, 루프 변형(loop variant), 종료 사양 및 읽기/쓰기 프레이밍 사양을 통해 형식 명세를 지원한다. Dafny는 함수형 프로그래밍과 명령형 프로그래밍 패러다임의 아이디어를 결합하며, 객체 지향 프로그래밍을 지원한다. 제네릭 클래스, 동적 할당, 귀납적 자료형, 그리고 부작용을 추론하기 위한 암시적 동적 프레임(implicit dynamic frames)이라 불리는 분리 논리의 변형 등이 주요 기능으로 포함된다. Dafny는 ESC/모듈라-3, ESC/Java, Spec# 개발 경험이 있는 마이크로소프트 리서치의 루스탄 레이노가 만들었다.

Dafny는 소프트웨어 검증 경진대회(예: VSTTE'08, VSCOMP'10, COST'11, VerifyThis'12)에서 정기적으로 다루어진다.

Dafny는 코드 개발과 함께 검증을 요구하는 검증 인지적(verification-aware) 프로그래밍 언어로 설계되었다. 따라서 이 언어는 정확한 구축 소프트웨어 개발 패러다임에 부합한다. 검증 증명은 수학적 정수와 실수, 비트 벡터, 시퀀스, 집합, 다중 집합, 무한 시퀀스 및 집합, 귀납법, 공귀납법, 계산적 증명을 포함하는 수학적 도구 모음에 의해 지원된다. 충분한 명세가 제공되면 검증 의무는 자동으로 해결된다. Dafny는 프로그램 분석을 사용하여 많은 명세 단언을 추론함으로써 사용자가 명세를 작성해야 하는 부담을 줄여준다. 일반적인 증명 프레임워크는 호어 논리이다.

Dafny는 증명 의무를 해결하기 위해 Z3 자동 정리 증명기를 사용하는 Boogie 중간 언어를 기반으로 한다.

데이터형

Dafny는 부작용이 있을 수 있는 구현용 메서드와, 명세에 사용되는 순수 함수(순수 함수)를 제공한다. 메서드는 익숙한 명령형 스타일의 문장들로 구성되는 반면, 함수 본문은 단순히 하나의 표현식으로 이루어진다. 메서드 내의 부작용을 일으키는 문장(예: 배열 매개변수의 요소 할당)은 modifies 절을 사용하여 어떤 매개변수가 변경될 수 있는지 명시해야 한다. Dafny는 시퀀스(예: seq<int>), 집합(예: set<int>), 맵(map<int,int>), 튜플, 귀납적 자료형, 가변 배열(예: array<int>) 등 다양한 불변 컬렉션 타입을 제공한다.

명령형 기능

다음은 사전 조건, 사후 조건, 루프 불변성, 루프 변형 등 Dafny의 여러 기능을 보여준다.

method max(arr:array<int>) returns (max:int)
 // 배열은 최소한 하나의 요소를 가져야 함
 requires arr.Length > 0
 // 반환값은 배열의 어떤 요소보다 작을 수 없음
 ensures forall j : int ::   j >= 0 && j < arr.Length  ==>  max >= arr[j]
 // 반환값은 배열 내의 일부 요소와 일치해야 함
 ensures exists j : int ::   j>=0 && j < arr.Length && max == arr[j]
{
  max := arr[0];
  var i: int := 1;
  //
  while(i < arr.Length)
  // 인덱스는 최대 arr.Length (루프 후 i==arr.Length임을 보이기 위해 필요)
  invariant i <= arr.Length
  // 지금까지 본 요소 중 max보다 큰 것은 없음
  invariant forall j:int :: j >= 0 && j < i  ==>  max >= arr[j]
  // 지금까지 본 요소 중 일부는 max와 일치함
  invariant exists j:int :: j >= 0 && j < i && max == arr[j]
  // arr.Length - i는 모든 단계에서 감소하며 0보다 크거나 같음
  decreases arr.Length - i
  {
    // 더 큰 요소를 발견하면 max 업데이트
    if (arr[i] > max) {
      max := arr[i];
    }
    // 배열 순회 지속
    i := i + 1;
  }
}

이 예제는 배열의 최대 요소를 계산한다. 메서드의 사전 조건과 사후 조건은 각각 requires 및 ensures 절로 주어진다. 마찬가지로 루프 불변성과 루프 변형은 각각 invariant 및 decreases 절을 통해 주어진다.

루프 불변성

Dafny에서 루프 불변성을 다루는 방식은 전통적인 호어 논리와 다르다. 루프에서 변형되는 변수는 루프 이전에 알려진 정보가 대부분 폐기되도록 처리된다. 이러한 변수의 속성을 증명하는 데 필요한 정보는 루프 불변성에 명시적으로 표현되어야 한다. 대조적으로, 루프에서 변형되지 않는 변수는 이전에 알려진 정보를 모두 유지한다. 다음 예제는 루프 사용법을 보여준다.

method sumAndZero(arr: array<int>) returns (sum: nat)
  requires forall i :: 0 <= i < arr.Length  ==>  arr[i] >= 0
  modifies arr
{
  var i: int := 0;
  sum := 0;
  //
  while(i < arr.Length) {
    sum := sum + arr[i];
    arr[i] := arr[i];
    i := i + 1;
  }
}

이 코드는 (sum + arr[i]) >= 0이 할당 시점에서 성립함을 Dafny가 확립할 수 없기 때문에 검증에 실패한다. 사전 조건으로부터 직관적으로 arr[i] := arr[i];가 NOP이므로 루프 내에서 forall i :: 0 <= i < arr.Length ==> arr[i] >= 0이 성립한다. 그러나 이 할당으로 인해 Dafny는 arr을 가변 변수로 취급하고 루프 이전의 정보를 폐기한다. Dafny에서 이 프로그램을 검증하려면 (a) 불필요한 할당 arr[i] := arr[i];를 제거하거나, (b) invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0을 루프 불변성에 추가하면 된다.

또한 Dafny는 제한적인 정적 프로그램 분석을 사용하여 가능한 경우 간단한 루프 불변성을 추론한다. 위 예제에서 변수 i가 루프 내에서 변경되므로 invariant i >= 0이 필요한 것처럼 보일 수 있다. 기초 논리상으로는 그러한 불변성이 필요하지만, Dafny는 이를 자동으로 추론하므로 소스 레벨에서는 생략할 수 있다.

증명 기능

Dafny는 증명 보조기로서의 사용을 뒷받침하는 기능을 포함한다. function이나 method 내의 간단한 속성 증명은 이러한 도구에서 드문 일이 아니지만, Dafny는 한 function과 다른 function 사이의 속성 증명도 허용한다. 증명 보조기의 일반적인 특성상, 이러한 증명은 종종 수학적 귀납법적 성격을 띤다. Dafny는 귀납적 가설을 적용하기 위한 메커니즘으로 메서드 호출을 사용하는 독특한 방식을 취한다. 다음은 그 예시이다.

datatype List = Nil | Link(data: int, next: List)

function sum(l: List): int {
  match l
    case Nil => 0
    case Link(d, n) => d + sum(n)
}

predicate isNatList(l: List) {
  match l
    case Nil => true
    case Link(d, n) => d >= 0 && isNatList(n)
}

lemma NatSumLemma(l: List, n: int)
  requires isNatList(l) && n == sum(l)
  ensures n >= 0
{
  match l
    case Nil =>
      // 자동으로 해결됨
    case Link(data, next) => {
      // 귀납적 가설 적용
      NatSumLemma(next, sum(next));
      // Dafny가 무엇을 알고 있는지 확인
      assert data >= 0;
    }
}

여기서 NatSumLemma는 sum()과 isNatList() 사이의 유용한 속성(즉, isNatList(l) ==> (sum(l) >= 0))을 증명한다. 보조정리와 정리를 인코딩하기 위해 ghost method를 사용하는 것은 Dafny의 표준이며, 귀납법(일반적으로 구조적 귀납법)을 위해 재귀가 사용된다. 사례 분석은 match 문을 사용하여 수행되며 비귀납적 사례는 종종 자동으로 해결된다. 검증기는 function이나 predicate의 내용을 필요에 따라 전개할 수 있도록 전체 내용에 접근할 수 있어야 한다. 이는 접근 제어자와 함께 사용될 때 영향을 미치는데, 특히 protected 수정자를 사용하여 function의 내용을 숨기면 그에 대해 확립할 수 있는 속성이 제한될 수 있다.

같이 보기

• 계약에 의한 설계

각주

더 읽어보기

• Meyer, Bertrand; Nordio, Martin 편집 (2012). 《Tools for Practical Software Verification: International Summer School, LASER 2011, Elba Island, Italy, Revised Tutorial Lectures》. 슈프링어. ISBN 978-3642357459. 
• Sitnikovski, Boro (2022). 《Introducing Software Verification with Dafny Language: Proving Program Correctness》. Apress. ISBN 978-1484279779. 

외부 링크

• Dafny: A Language and Program Verifier for Functional Correctness - 마이크로소프트 리서치
• (영어) Dafny - 깃허브, 검증 인지적 프로그래밍 언어