4
정적 분석기가 입증 할 수없는 특정 계약이 있습니다. 특정 종류의 계약 위반 오류를 전체 기능에서 제외 할 수는 있지만 너무 광범위합니다. baseline.xml 기능을 사용하여 특정 위반 오류를 제외 할 수 있지만 팀 환경에서 감사 또는 문서 작성이 본질적으로 불가능합니다. 한마디로일부 계약을 정적 분석에서 쉽게 제외 할 수 있습니까?
이 가능 정적 분석기 막 다른 골목 것으로 보인다 제 3 자 라이브러리에서 만든 어떤 계약도 있습니다
Contract.Requires(DoesHalt() == true, ExcludeFromStaticAnalysis=true);
같은 것을 할 것입니다. 정적 분석을 위해 이들을 비활성화하고 싶습니다. 하나의 좋아하는 예제는 .NET 그래프 라이브러리에 구축 된 계약입니다. 깊이 검색 기능에 대한 인수는 그래프에서 어떤 정점을 사용하여 검색을 시작 할지를 지정하며 Contract.Requires은 정점이 그래프의 멤버가되도록 요구합니다. 현명한 계약, 어쩌면 디버그 빌드에서 실행 가치는 있지만, 정적으로 증명 될 수있는 먼 길입니다. 그러나 깊이 우선 검색을 사용할 때마다 정적 위반을 무시할 수있는 방법을 찾아야합니다. (Contract.Assume으로 해결할 수 없음)
증명할 수없는 물건에서 증명 가능한 항목을 분할 할 수 없다면 정적 인 분석이 너무 작고 시끄러운 깨끗한 코드 기반이라 할지라도 정적 분석을 찾는 것입니다.
"Contract.Requires (DoesHalt() = true 또는 AssumeTrueBecauseYouCantProveThis)"라고 간단하게 쓸 수없는 이유는 무엇입니까? [여기서 AssumeTrueBecauseYouCantProvethis는 정적 const 값 "true"입니다.] 좋은 "증명 인"은 이별의 일부가 사소하게 사실임을 알고 그 시점에서 계약 확인에 대한 작업을 중단해야합니다. –
런타임 검사기가 실제로 검사를 수행해야하기 때문입니다. 이 검사는 항상'|| 사실 '. –