Usando Contract.ForAll in Code Contracts

Question

De acuerdo, tengo otra pregunta de Contratos de Código. Tengo un contrato en un método de interfaz que se parece a esto (otros métodos omitidos para mayor claridad):

[ContractClassFor(typeof(IUnboundTagGroup))] 
public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup 
{ 
    public IUnboundTagGroup[] GetAllGroups() 
    { 
     Contract.Ensures(Contract.Result<IUnboundTagGroup[]>() != null); 
     Contract.Ensures(Contract.ForAll(Contract.Result<IUnboundTagGroup[]>(), g => g != null)); 

     return null; 
    } 
} 

tengo código de consumo de la interfaz que se parece a esto:

public void AddRequested(IUnboundTagGroup group) 
    { 
      foreach (IUnboundTagGroup subGroup in group.GetAllGroups()) 
      { 
       AddRequested(subGroup); 
      } 
      //Other stuff omitted 
    } 

AddRequested no requiere una parámetro de entrada nulo (implementa una interfaz que tiene un contrato de Requiere) y así obtengo un error 'requiere no comprobado: grupo! = nulo' en el subgrupo que pasa al AddRequested. ¿Estoy usando la sintaxis ForAll correctamente? Si es así y el solucionador simplemente no comprende, ¿hay alguna otra manera de ayudar al solucionador a reconocer el contrato o simplemente necesito usar un Asumir siempre que se llame a GetAllGroups()?

Answer 1

El Code Contracts User Manual dice: "El verificador de contrato estático todavía no se ocupa de los cuantiers para todos o existan". Hasta que lo haga, me parece que las opciones son:

1. Ignore la advertencia.
2. Agregue Contract.Assume(subGroup != null) antes de la llamada al AddRequested().
3. Agregue un cheque antes de llamar al AddRequested(). Tal vez if (subGroup == null) throw new InvalidOperationException() o if (subGroup != null) AddRequested(subGroup).

La opción 1 realmente no ayuda. La opción 2 es arriesgada porque eludirá el AddRequested() Requiere contrato incluso si IUnboundTagGroup.GetAllGroups() ya no garantiza esa condición posterior. Me gustaría ir con la opción 3.