如何使用代码契约指示方法永远不会返回 null？

Question

如何指示一个方法永远不会返回 null？ 目前这是我的代码。

第 19 行收到 Ensures notproved 消息，即使 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);

？ 基本上，我会尝试将其削减，直到找到最简单的情况，但不能按您的预期工作，然后从那里开始。

——马库斯Q

Answer 2

您需要将 CreateFunction 中的 Assume 更改为 Ensures。 之后你应该没事了。 请记住，Assume 用于内部假设，以便在本地帮助静态检查器。 从其他方法中看不到它们。 只有 Requires 和 Ensures 是跨方法合约。