코드 계약을 통해 루프가 입증되지 않음

Question

.Net 코드 계약 (VS2010 Ultimate .Net 4)을 사용하여 정적 검사기가 증명할 수 있거나 증명할 수없는 것에 대한 아이디어를 얻으려고합니다.

나는 다음 예제를 시도하고있다 : -

public int Mult(int num1, int num2) 
    { 
     Contract.Requires(num2 >= 0); 
     Contract.Ensures(Contract.Result<int>() == (num1 * num2)); 
     int result = 0; 
     for (int i = 0; i < num2; i++) 
     { 
      result = result + num1; 
     } 
     return result; 
    } 

즉, 다중 기능의 간단한 구현을 반복 추가하여. ..

CodeContracts: ensures unproven: Contract.Result<int>() == (num1 * num2) 

내 함수가 실제로 제품을 제대로 계산되지 않았거나 정적 검사가를 확인할 수없는 또 다른 이유가있다 -은 :

정적 검사는 사후 조건이 충족되었는지 확인 할 수 필요하십니까? 루프가 있으면 문제가 발생합니까?

루프가있을 때 정적 검사기가 작업을 확인하는 것이 어렵다면 항상 많은 경고가 발생하는 것은 상당히 짜증나게됩니다.

나는 처음에 버그의 원인이되는 나의 잘못된 가정이기 때문에 내가 생각하고있는 것을 말해주기 위해 Assumes를 넣는 옵션을 좋아하지 않습니다!

정적 검사기가 어떤 것을 증명할 수 없으면 어떻게 도와 줄 수 있습니까? 예를 들어 함수를 재귀 함수로 다시 작성할 수 있습니다. 그러면 검사기가보다 쉽게 ​​확인할 수 있습니까? (그리고 함수형 프로그래밍을 옹호하는 사람들은 이것이 처음부터 쓰여 져야하는 방식이라고 말할 수있다. 정적 검사기를 쉽게 만들 수 있도록 다른 방법으로 코드를 변경할 수 있습니까?

감사합니다! :)

Answer 1

정적 검사는이를 입증 할 수 없을 것이다, 그러나 런타임 검사 것.

정적 검사기는 컴파일 할 때 적용됩니다. 귀하의 보장을 증명할 수 있으려면 귀하의 알고리즘과 귀하가하는 일을 완전히 분석 할 수 있어야합니다. 그것은 그렇게 강력하지 않습니다.

런타임 검사기는 기능이 종료되고 적절한 단위 테스트를 통해 보장의 유효성을 입증해야 할 때마다 보증을 유효하게합니다.

Answer 2

표현의 한 가지 방법은 코드 계약이 수학자/논리 학자가 아니라는 것입니다.

하면 코드 계약 수는

num1 + num1 + ... + num1  (num2 terms in total) 

당신이 그냥 어떤 수학 문제 및 코드 계약을 공급할 수없는 다음

num1 * num2 

에 해당된다는 점 "증명"기대처럼 코드에 대한 실제 이유 너를 위해 그것을 해결할 수 있을까?

저는 이론적 인 컴퓨터 과학 전문가는 아니지만 다음 주장에 대해 전적으로 확신하지는 않지만이 질문은 Halting Problem (이 부분은 this blog article by Eric Lippert 하단에도 있음)이라고 생각합니다.

따라서 Code Contracts가 임의의 수학적 문제를 증명할 수 없다는 것은 확실합니다.코드 계약이 코드에 대한 추론에서 얼마나 먼지 알 수는 없지만 몇 가지 매우 기본적인 구체적인 것들을 확인하는 것보다 훨씬 나아질 것이라고 생각합니다. 예 : 블로그 기사 "Static Checking .NET Code Contracts" by Doug Finke에서 두 번째 스크린 샷을 살펴보십시오.