1

内部リストに要素を追加するメソッドを設計しています。クラスの構造は、次のようなものです。

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

    public int NumberOfCustomers { get { return _customers; } }    

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

さて、Contract.Ensures()この呼び出しで_customersのサイズを1つ増やすことを考えていました。問題は、奇妙なコードになってしまうことです。

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


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

Contract.ValueAtReturn()主な問題は、プロパティが実際にはメソッドであるため、唯一のパラメータが変数をとして受け入れるため、プロパティを直接参照することはできないということですout。同じことを達成したい場合、状況はさらに奇妙になりますが、今回は値を返す必要があるメソッドを使用します。

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

これはかなり不器用なようです:(

コードコントラクトは物事をより明確にすることを目的とすべきであり、これは正反対のようです。私は何か間違ったことをしていますか？

ありがとう

4

2 に答える 2

1

あなたはすべて正しいことをしていると思います。

ただし、そのメソッドを呼び出すことの正確な出力の意味を説明することにより、契約を極端に取っていると感じています。コントラクトの基本的な考え方は、正であること、値を返すことなど、基本的な保証を保証することでした。

于 2010-05-06T11:00:36.257 に答える
1

理由もなく物事を過度に複雑にしているようです。ValueAtReturnメソッドへのパラメーターについて話すために使用されoutますが、それ以外には何もありません — そして、outパラメーターはありません!

あなたが探しているのはOldValue.

この行を次のように仮定します。

public int NumberOfCustomers { get { return _customers; } }

次のことを意味します。

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

あなたがしなければならないことは、次のとおりです。

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

IList<T>:)の事後条件のおかげで、静的チェッカーはこれをうまく証明できます。

于 2010-05-10T12:18:13.237 に答える