CODEWITHSUNDEEP
.net.net-4.0code-contractsmicrosoft-contracts
Jonathan Allen
Jonathan Allen

Reputation: 70337

How do I indicate that a method never returns a null using code contracts?

How do I indicate that a method never returns a null? Currently this is my code.

Line 19 gets an Ensures not proven message, even though CreateFunction assumes that the result is not nothing.

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

Upvotes: 1

Views: 529

Answers (2)

Manuel Fahndrich
Manuel Fahndrich

Reputation: 665

You need to change the Assume in CreateFunction to an Ensures. After that you should be okay. Remember, Assume is for internal assumptions in order to help the static checker locally. They are not visible from other methods. Only Requires and Ensures are cross-method contracts.

Upvotes: 0

MarkusQ
MarkusQ

Reputation: 21950

Does 

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

work? Basically, I'd try paring it down till you find the simplest case that doesn't work as you'd expect and go from there.

-- MarkusQ

Upvotes: 6

Related Questions