Utilisations maladroites de Contract.ValueAtReturn()

Question

Je suis en train de concevoir une méthode qui ajoutera un élément à une liste interne. La structure de la classe est quelque chose le long des lignes de:

class MyCustomerDatabase { 
    private IList<Customer> _customers = new List<Customer>(); 

    public int NumberOfCustomers { get { return _customers; } }  

    public void AddCustomer(Customer customer) { 
     _customers.Add(customer); 
    } 
} 

Maintenant, je pensais à l'ajout d'un Contract.Ensures() de la taille des _Clients en croissance de 1 à cet appel. Le problème est que je me retrouve avec un code qui vous bizarre:

public void AddCustomer(Customer customer) { 
    int numberOfCustomersAtReturn; 
    Contract.Ensures(Contract.ValueAtReturn<int>(out numberOfCustomersAtReturn) == 
Contract.OldValue<int>(NumberOfCustomers) + 1); 


    _customers.Add(customer); 
    numberOfCustomersAtReturn = NumberOfCustomers; 
} 

Le principal problème est que les propriétés sont des méthodes de fait, de sorte que vous ne pouvez pas simplement les référencer direcly lors de l'utilisation Contract.ValueAtReturn() comme seul paramètre accepte les variables que out. La situation devient encore plus étrange si je veux obtenir le même, mais cette fois avec une méthode qui doit retourner une valeur:

public int MyReturningMethod() { 
    ... 
    return abc(); //abc will add by one the number of customers in list 
} 
//gets converted to 
public int MyReturningMethod() { 
    int numberOfCustomersAtReturn; 
    Contract.Ensures(Contract.ValueAtReturn<int>(out numberOfCustomersAtReturn) == Contract.OldValue<int>(NumberOfCustomers) + 1); 

    int returnValue = abc(); 
    numberOfCustomersAtReturn = NumberOfCustomers; 
    return returnValue; 
} 

Cela semble assez maladroit :(

contrats Code devraient viser à faire avancer les choses plus claires et cela semble juste le contraire. Est-ce que je fais quelque chose de mal?

Merci

Answer 1

Il semble que vous complétiez les choses sans raison. ValueAtReturn est utilisé pour parler de out paramètres à une méthode, et rien d'autre — et vous n'avez pas de out paramètres! Ce que vous cherchez est OldValue.

En supposant que cette ligne:

public int NumberOfCustomers { get { return _customers; } } 

est censé être:

public int NumberOfCustomers { get { return _customers.Count; } } 

Tout ce que vous avez à faire est:

class MyCustomerDatabase 
{ 
    private readonly IList<Customer> customers = new List<Customer>(); 

    public int NumberOfCustomers { get { return customers.Count; } } 

    public void AddCustomer(Customer customer) 
    { 
     Contract.Ensures(NumberOfCustomers == 
         Contract.OldValue(NumberOfCustomers) + 1); 

     customers.Add(customer); 
    } 
} 

Le vérificateur statique peut prouver très bien , grâce aux postconditions au IList<T> :)

Answer 2

Je pense que vous faites tout droit.

Bien que j'ai le sentiment que vous prenez des contrats à l'extrême en décrivant les implications exactes de la sortie de l'appel de cette méthode. Imho l'idée de base des contrats était plus de garantir de base garantit, comme étant positif, renvoyant une valeur du tout et ainsi de suite