Utilizzo di Contract.ForAll nei contratti di codice

Question

OK, ho ancora un'altra domanda sui contratti di codice. Ho un contratto su un metodo di interfaccia che assomiglia a questo (altri metodi omessi per chiarezza):

[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; 
    } 
} 

Ho codice consumando l'interfaccia che assomiglia a questo:

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

AddRequested richiede un non- parametro input null (implementa un'interfaccia che ha un contratto Requires) e quindi ottengo un errore 'require unproven: group! = null' sul sottogruppo passato a AddRequested. Sto usando correttamente la sintassi ForAll? Se è così e il risolutore semplicemente non sta capendo, c'è un altro modo per aiutare il risolutore a riconoscere il contratto o semplicemente ho bisogno di usare un Assume ogni volta che viene chiamato GetAllGroups()?

Answer 1

Gli stati Code Contracts User Manual, "Il controllore contratto statico non ha ancora a che fare con i quantificatori For All o Exists." Fino a quando non lo fa, mi sembra che le opzioni siano:

1. Ignora l'avviso.
2. Aggiungi Contract.Assume(subGroup != null) prima della chiamata a AddRequested().
3. Aggiungere un controllo prima della chiamata a AddRequested(). Forse if (subGroup == null) throw new InvalidOperationException() o if (subGroup != null) AddRequested(subGroup).

L'opzione 1 non è di grande aiuto. L'opzione 2 è rischiosa perché aggirerà il contratto AddRequested() Richiesto anche se IUnboundTagGroup.GetAllGroups() non garantisce più tale condizione. Vorrei andare con l'opzione 3.