메소드가 코드 계약을 사용하여 null을 반환하지 않는다는 것을 어떻게 나타 냅니까?

Question

메서드가 null을 반환하지 않는다는 것을 어떻게 나타 냅니까? 현재 이것은 내 코드입니다.

Line 19는 CreateFunction이 결과가 아무 것도 아니라고 가정하더라도 확인되지 않은 메시지를 가져옵니다.

1   <Pure()> Public Function CreateFunction(Of TArg1, TArg2, TResult)(ByVal body As Func(Of Expression, Expression, BinaryExpression)) As Func(Of TArg1, TArg2, TResult) 
2    Contract.RequiresAlways(body IsNot Nothing) 
3    Contract.Assume(Contract.Result(Of Func(Of TArg1, TArg2, TResult))() IsNot Nothing) 
4 
5    Dim arg1 = Expression.Parameter(GetType(Integer), "arg1") 
6    Dim arg2 = Expression.Parameter(GetType(Integer), "arg2") 
7 
8 
9    Dim temp = Expression.Lambda(body(arg1, arg2), arg1, arg2) 
10    Contract.Assume(temp IsNot Nothing) 
11    Return DirectCast(temp.Compile, Global.System.Func(Of TArg1, TArg2, TResult)) 
12   End Function 
13 
14   <Pure()> Public Function Add() As Func(Of T, T, T) 
15    Contract.Ensures(Contract.Result(Of Func(Of T, T, T))() IsNot Nothing) 
16 
17    Dim temp = CreateFunction(Of T, T, T)(AddressOf Expression.AddChecked) 
18    Return temp 
19   End Function 

Answer 1

는

Contract.Ensures(Contract.Result() != null); 

사용할 수 있습니까? 기본적으로, 나는 당신이 기대했던대로 작동하지 않는 가장 단순한 케이스를 찾을 때까지 그것을 페어링하려고합니다.

은 - MarkusQ

Answer 2

당신은 Ensures에 CreateFunction에 Assume을 변경해야합니다. 그 후에는 괜찮을거야. Assume은 정적 검사기를 로컬에서 지원하기 위해 내부 가정용임을 기억하십시오. 다른 방법으로는 보이지 않습니다. Requires 및 Ensures 만 교차 방법 계약입니다.