Comment est-ce que j'indique qu'une méthode ne renvoie jamais de null en utilisant des contrats de code?

Question

Comment puis-je indiquer qu'une méthode ne retourne jamais nulle? Actuellement c'est mon code.

Ligne 19 obtient un pas un message Garantit prouvé, même si createFunction suppose que le résultat est rien.

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

Est-ce que

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

travail? Fondamentalement, je vais essayer de le réduire jusqu'à ce que vous trouviez le cas le plus simple qui ne fonctionne pas comme vous vous y attendiez et que vous partiez de là.

- MarkusQ

Answer 2

Vous devez changer le Assume en CreateFunction à un Ensures. Après ça, ça devrait aller. Rappelez-vous, Assume est des hypothèses internes afin d'aider le vérificateur statique au niveau local. Ils ne sont pas visibles par d'autres méthodes. Seuls Requires et Ensures sont des contrats inter-méthode.