Contratti di raccolta e filettatura

Question

Supponiamo di disporre di una classe di raccolta personalizzata che fornisce una sincronizzazione interna del thread. Per esempio, un metodo Add semplificato potrebbe essere simile a questo:

public void Add(T item) 
    { 
     _lock.EnterWriteLock(); 
     try 
     { 
      _items.Add(item); 
     } 
     finally 
     { 
      _lock.ExitWriteLock(); 
     } 
    } 

ultimi contratti Codice lamenta che CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count). Il problema è che questo non può essere provato. Posso assicurarmi che, internamente, all'interno del blocco, Count sarà maggiore del suo valore precedente. Non posso garantire questo, tuttavia, all'uscita del metodo. Una volta chiuso il blocco e prima che il metodo venga completato, un altro thread potrebbe emettere due Rimuove (probabilmente di elementi diversi), invalidando il contratto.

Il problema fondamentale qui è che i contratti di riscossione possono essere considerati validi solo all'interno di un particolare contesto di blocco e solo se il blocco viene utilizzato in modo coerente in tutta l'applicazione per tutti gli accessi alla raccolta. La mia raccolta deve essere utilizzata da più thread (con Add-Remove non in conflitto essendo un caso d'uso valido), ma mi piacerebbe ancora implementare ICollection<T>. Dovrei semplicemente fingere di poter soddisfare questo requisito con un assunto, anche se so che non posso? Mi sembra che nessuna delle collezioni BCL possa effettivamente garantire questo.

---

EDIT:

Sulla base di alcuni ulteriori indagini, sembra che il problema più grande è che il masterizzatore contratto può introdurre affermazioni non corrette, che porta a runtime fallimenti. Sulla base di ciò, ritengo che la mia unica opzione sia limitare l'implementazione dell'interfaccia a IEnumerable<T>, poiché il contratto su ICollection<T> implica che la classe di implementazione non possa fornire la sincronizzazione interna del thread (l'accesso deve sempre essere sincronizzato esternamente). Ciò è accettabile per il mio caso particolare (tutti i clienti che desiderano modificare la collezione conoscono direttamente il tipo di classe), ma sono sicuramente interessato a sapere se ci sono altre soluzioni a questo.

Answer 1

Come si sottintende, nessun implementatore può soddisfare questo contratto. Infatti generalmente a fronte di multi-threading a meno che il contratto può essere applicato come:

Take Lock 
gather Old Stuff 

work 

check Contract, which may compare Old Stuff 
Release Lock 

Io non vedo come qualsiasi contratto potrebbe essere onorato. Da quello che vedo here questa è un'area che non è ancora completamente cotta.

Penso che usare un assunto sia il migliore che si possa fare, in effetti si sta dicendo "chiamando Aggiungi sto facendo quello che il contratto si aspetta".

Answer 2

using System.Diagnostics.Contracts; 

namespace ConsoleApplication1 
{ 
    class Class1 
    { 
     public int numberOfAdds { get; private set; } 
     public int numberOfRemoves { get; private set; } 
     public int Count 
     { 
      get 
      { 
       return numberOfAdds - numberOfRemoves; 
      } 
     } 

     public void Add() 
     { 
      Contract.Ensures(numberOfAdds == Contract.OldValue(numberOfAdds) + 1); 
     } 

     public void Remove() 
     { 
      Contract.Requires(Count >= 1); 
      Contract.Ensures(numberOfRemoves == Contract.OldValue(numberOfRemoves) + 1); 
     } 

     [ContractInvariantMethod] 
     void inv() 
     { 
      Contract.Invariant(Contract.Result<int>() == numberOfAdds - numberOfRemoves); 
     } 
    } 
} 

Avvertenza: non utilizzare una quantità inferiore a quella del confronto; I conteggi saranno eccessivi, ma questi contratti dovrebbero funzionare in quel caso. Prova con un tipo intero piccolo come int8. Assicurati di utilizzare un tipo intero che non sia in overflow.