다프니

Dafny
다프니
Dafny logo.jpg
패러다임명령적, 기능적
설계자K. 러스탄 M.라이노
개발자마이크로소프트 리서치
첫 등장2009; 13년 전(2009)
안정적 해제
3.0.0 / 2021년 2월 3일; 13개월 전(2021-02-03)
타이핑 규율정적, 강력, 안전
면허증MIT 라이선스
파일 이름 확장명.dfy
웹사이트research.microsoft.com/dafny

다프니는 C#를 대상으로 하는 필수 컴파일 언어로서 전제조건, 자세조건, 루프 불변제, 루프 변형을 통해 형식적인 명세를 지원한다.언어는 주로 기능적 패러다임과 명령적 패러다임에서 아이디어를 결합하며 객체 지향 프로그래밍에 대한 제한된 지원을 포함한다.특징에는 부작용 추론을 위한 일반 클래스, 동적 할당, 유도 데이터 유형 및 암시적 동적 프레임으로[1] 알려진 분리 논리 변형이 포함된다.[2]다프니는 마이크로소프트 리서치의 러스탄 레이노가 ESC/모듈라-3, ESC/자바, 스펙# 등의 개발 전작을 거쳐 만든 것이다.Dafny는 가르치는 데 널리 사용되며 소프트웨어 검증 대회(예: VSTE'08,[3] VSCOMP'10,[4] COST'11, [5]Verify)에 정기적으로 참가하고 있다.12시[6] 입니다.

다프니는 형식적인 사양과 검증에 대한 간단한 소개를 제공하도록 설계되었으며, 가르치는 데 널리 사용되어 왔다.Dafny는 증명 의무를 이행하기 위해 Z3 자동 정리 프로베러를 사용하는 Boogie 중간 언어를 기반으로 한다.[7][8]

데이터 유형

Dafny는 부작용이 있을 수 있는 구현 방법과 순수한 규격에 사용할 수 있는 기능을 제공한다.방법은 익숙한 명령 스타일을 따르는 명령어 순서에 따라 구성되는 반면, 대조적으로 함수의 본문은 단순한 표현이다.방법의 부작용 문장(예: 배열 매개변수의 요소 할당)은 다음에서 어떤 매개변수가 변이될 수 있는지 유의하여 설명해야 한다.modifies조항의Dafny는 또한 시퀀스(예: 시퀀스)를 포함한 불변 수집 유형의 범위를 제공한다.seq<int>)), 세트(예:set<int>) 및 지도(map<int,int>. 추가적으로 변이 가능한 배열(예:array<int>)이 제공된다.

필수 기능

다프니는 호아레 논리의 아이디어에 근거한 필수 프로그램의 증명서를 지원한다.다음은 전제 조건, 자세 조건, 루프 불변제 및 루프 변형의 사용을 포함하여 다프니의 많은 그러한 특징을 보여준다. 

방법 맥스.(arr:배열하다<인트로>) 돌아온다(맥스.:인트로)  // 배열에 하나 이상의 요소가 있어야 함  필요로 하다 arr!=무효의 && arr.길이 > 0;  // 반환은 배열의 어떤 요소보다 작을 수 없음  보증하다 (전부 j :인트로 :: (j >= 0 && j < arr.길이 ==> 맥스. >= arr[j]));  // 반환은 배열의 일부 요소와 일치해야 함  보증하다 (존재한다 j : 인트로 :: j>=0 && j < arr.길이 && 맥스.==arr[j]); {   맥스.:=arr[0];   시합을 하다 i:인트로 :=1;   //   하는 동안에(i < arr.길이)   // 최대한 들여쓰기.길이(i=arr 표시 필요).루프 후 길이)   불변의 (i<=arr.길이);   // 최대값보다 큰 요소가 보이지 않음   불변의 (전부 j:인트로 :: j>=0 && j<i ==> 맥스. >= arr[j]);   // 지금까지 확인된 일부 요소가 최대값과 일치함   불변의 (존재한다 j:인트로 :: j>=0 && j<i && 맥스. == arr[j]);   // i == arr일 때 종료.길이   감소하다 (arr.길이-i);    {     // 더 큰 요소가 발견된 경우 최대값 업데이트     만일(arr[i] > 맥스.){맥스. := arr[i];}     // 배열을 통해 계속 진행     i := i + 1;   } }

이 예는 배열의 최대 요소를 계산한다.그 방법의 전제조건과 사후조건은 다음과 함께 주어진다.requires그리고ensures절(절)마찬가지로 루프 불변형 및 루프 변형은 를 통해 주어진다.invariant그리고decreases절(절)

루프 불변성

다프니에서의 루프 불변제 치료는 전통적인 호어 논리와는 다르다.루프에서 변이된 변수는 루프 이전에 변수에 대해 알려진 (대부분) 정보가 폐기되도록 처리된다.그러한 변수의 특성을 입증하기 위해 필요한 정보는 루프 불변량 내에 명시적으로 표현되어야 한다.이와는 대조적으로, 루프에서 변이되지 않은 변수들은 사전에 알려진 모든 정보를 유지한다.다음은 다음을 예시한다.

방법 섬앤드제로(ns:배열하다<인트로>) 돌아온다 (합계를 내다:냇)   필요로 하다 ns != 무효의   필요로 하다 전부 i :: 0 <= i < ns.길이 ==> ns[i] >= 0   수정하다 ns  {   시합을 하다 i:인트로 := 0;   시합을 하다 arr:배열하다<인트로> := ns; // 매개 변수를 할당할 수 없으므로   합계를 내다 := 0;   //   하는 동안에(i < arr.길이) {     합계를 내다 := 합계를 내다 + arr[i];     arr[i] := arr[i];     i := i + 1;   } }

Dafny는 이 사실을 확인할 수 없기 때문에 검증에 실패함(sum + arr[i]) >= 0임무를 맡다그 전제조건에서 직관적으로 보면forall i :: 0 <= i < arr.Length ==> arr[i] >= 0그 이후로 계속 유지되다.arr[i] := arr[i];NOP이다.그러나 이 과제는 Dafny가 치료하게 한다.arr변이 가능한 변수와 그에 대해 알고 있는 정보를 루프 앞에서 삭제한다.Dafny에서 이 프로그램을 확인하려면 다음 중 하나를 수행하십시오. 중복 할당 제거arr[i] := arr[i];; 또는 루프 불변성 추가invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0

Dafny는 가능한 경우 단순한 루프 불변제를 추론하기 위해 제한된 정적 분석을 추가로 채택한다.위의 예에서, 그것은 루프 불변으로 보일 것이다.invariant i >= 0변수로도 필요하다.i루프 내에서 돌연변이가 발생했어기본 논리에는 그러한 불변성이 필요하지만, Dafny는 이것을 자동으로 주입하므로 소스 수준에서 생략할 수 있다.

증명 기능

Dafny는 증명 보조자로서 그것의 사용을 더욱 뒷받침하는 특징들을 포함하고 있다.a 내에서 간단한 특성을 증명하는 동안function또는method(위 그림처럼) 이런 성격의 도구에는 흔치 않은 것이 아니며, 다프니는 또한 한 가지 사이에 재산의 증명도 허용한다.function그리고 또 다른 것.증명 조수에게 흔히 있는 일이지만, 그러한 증명은 자연에서 귀납되는 경우가 많다.다프니는 귀납 가설을 적용하기 위한 메커니즘으로 방법 발동을 채택하는 데 있어서 아마도 특이한 것일 것이다.다음은 다음을 예시한다.

데이터타입 리스트 = 닐   링크(자료:인트로,다음에:리스트)  기능을 하다 합계를 내다(l:리스트): 인트로 {   짝을 맞추다 l     케이스 닐 => 0     케이스 링크(d,n) => d + 합계를 내다(n) }  술어를 붙이다 isNatList(l:리스트) {   짝을 맞추다 l     케이스 닐 => 진실의     케이스 링크(d,n) => d >= 0 && isNatList(n) }  귀신이 되다 방법 나트섬레마(l:리스트, n:인트로) 필요로 하다 isNatList(l) && n == 합계를 내다(l) 보증하다 n >= 0  {   짝을 맞추다 l     케이스 닐 =>       // 자동 퇴원     케이스 링크(자료,다음에) => {       // 귀납 가설 적용       나트섬레마(다음에,합계를 내다(다음에));       // Dafny가 알고 있는 내용 확인       주장하다 자료 >= 0;     } }

여기,NatSumLemma사이의 유용한 재산을 증명하다. sum()그리고isNatList()(즉, 저것)isNatList(l) ==> (sum(l) >= 0)). 의 사용.ghost method인코딩 레마 및 이론은 인덕션(일반적으로 구조 유도)을 위해 사용되는 재귀와 함께 Dafny에서 표준적이다.사례 분석은 다음을 사용하여 수행된다.match진술과 비 귀납적 사례는 종종 자동으로 배출된다.검증자는 또한 a의 내용에 대한 완전한 접근 권한을 가져야 한다.function또는predicate필요에 따라 롤링을 해제할 수 있도록이것은 접근 수식어와 함께 사용될 때 시사하는 바가 있다.구체적으로는 a의 내용을 숨긴다.function을 이용하여protected수식어는 그것에 대해 설정될 수 있는 속성을 제한할 수 있다.

참고 항목

참조

  1. ^ Smans, Jan; Jacobs, Bart; Piessens, Frank (2009). Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic (PDF). Proceedings of the Conference on European Conference on Object Oriented Programming. pp. 148–172. doi:10.1007/978-3-642-03013-0_8.
  2. ^ Leino, Rustan (2010). Dafny: An Automatic Program Verifier for Functional Correctness. Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. 348–370. doi:10.1007/978-3-642-17511-4_20.
  3. ^ Leino, Rustan; Monahan, Rosemary (2010). Dafny Meets the Verification Benchmarks Challenge (PDF). International Conference on Verified Software: Theories, Tools, and Experiments. pp. 112–116. doi:10.1007/978-3-642-15057-9_8.
  4. ^ Klebanov, Vladimir; et al. (2011). The 1st Verified Software Competition: Experience Report. Proceedings of the Conference on Formal Methods. pp. 154–168. CiteSeerX 10.1.1.221.6890. doi:10.1007/978-3-642-21437-0_14.
  5. ^ Bormer, Thorsten; et al. (2011). The COST IC0701 Verification Competition 2011. Proceedings of the Conference on Formal Verification of Object-Oriented Software. pp. 3–21. CiteSeerX 10.1.1.396.6170. doi:10.1007/978-3-642-31762-0_2.
  6. ^ Huisman, Marieke; Klebanov, Vladimir; Monahan, Rosemary (2015). "VerifyThis 2012: A Program Verification Competition" (PDF). Journal on Software Tools for Technology Transfer. 17 (6): 647–657. doi:10.1007/s10009-015-0396-8. S2CID 14301377.
  7. ^ "Z3 Homepage". 2019-02-07.
  8. ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Z3: An Efficient SMT Solver. Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis. pp. 337–340. doi:10.1007/978-3-540-78800-3_24.

추가 읽기

  • Meyer, Bertrand; Nordio, Martin, eds. (2012). Tools for Practical Software Verification: International Summer School, LASER 2011, Elba Island, Italy, Revised Tutorial Lectures. Springer. ISBN 978-3642357459.

외부 링크