5

Visual Studio (2008) 内から静的検証の警告に気付いたとき、スタック オーバーフローで誰かの質問に答えようとしていじり回していました。

string[] source = { "1", "A", "B" };
var sourceObjects = Array.ConvertAll(source, c => new Source(c)).ToArray();

「 required unproven source != null」というメッセージが表示されます。これが事実ではないことは私には明らかです。もちろんこれはほんの一例です。一方で、いくつかのかなり気の利いたものがかなりうまく機能しているようです。

1.2.20518.12 リリース (5 月 18 日) を使用しています。コード コントラクトは非常に興味深いと思いますが、他にこのようなケースがあった人はいますか? 現在の実装は実際に使用できると思いますか、それとも現時点では純粋に学術的であると考えますか?

私はこれをコミュニティ wiki にしましたが、いくつかの意見を聞きたいです :)

4

1 に答える 1

16

2 つの呼び出しを分割すると、より理にかなっています。

string[] source = { "1", "A", "B" };
var tmp = Array.ConvertAll(source, c => new Source(c));
var sourceObjects = tmp.ToArray();

現在、問題として最後の行を指しています。つまり、 への呼び出しArray.ConvertAllは source が null ではないことを認識していますが、 への呼び出しはそれが null ではToArray()ないことを認識していませんtmp。

（ソースコードで名前を使用しているため、例も少し混乱しています..の最初のパラメーターを参照しているため、変数をまったく別のものと呼んでいてもsource、エラーは引き続き使用されます。）sourceEnumerable.ToArray

基本的に、Array.ConvertAll が適切な非 null 事後条件を取得すると、これはすべて機能すると思います。それまでは、これでうまくいきます。

string[] source = { "1", "A", "B" };
var tmp = Array.ConvertAll(source, c => new Source(c));
Contract.Assume(tmp != null);
var sourceObjects = tmp.ToArray();

この種のことは煩わしいことに同意しますが、MS が BCL にコントラクトを追加するにつれて、急速に改善されると確信しています。静的チェッカー自体の問題ではないことに注意してください。

(実際にArray.ConvertAllは、前提条件もありませんsource。上記の 2 番目のコード スニペットで変数を null に設定しても、エラーは発生しません。)

于 2009-08-09T12:18:27.043 に答える