jml

2熱

1答えて

私はJMLの質問があります。 array_の要素に関する protected /*@ non_null */ Object[] array_; として、それを宣言する /*@ invariant array_ != null; */ との違いは何ですか？それぞれの場合、どのような財産がありますか？ありがとうございます。

3熱

2答えて

JML

におけるリターンで私はsize_ iはJMLでそれを行うことができますどのように if(size_ == 0) return null; に基づいて0の場合はnullを返すことが保証事後条件を設定する必要が声明場合は？何か案は？動作しない、次のとおりです。 //@ ensures size_ == null ==> \result == true; public boolean s

0熱

2答えて

アンドロイド：msnのjmlライブラリはアンドロイド2.1で動作しませんか？

私は、プロジェクトでgetpropertyactionクラスを追加して、Androidのjmlライブラリからmsnに接続できました。アンドロイド2.2でうまく動作し、私はログインすることができます、連絡先を取得し、メッセージやその他を受信します.. アンドロイド2.1私はログインボタンを押すと私はログインしません...私は 'トン...それだけで滞在の

2熱

1答えて

Eclipseオートフォーマットのコメントの後にスペースを削除するには？

私は自分のプロジェクトにOpenJMLプラグインを使用していますが、Eclipseの自動フォーマットでJMLコードが混乱します。 JMLは//@シンボルの後に書かれています。 //@ requires password != null; //@ ensures !isActive() && getPassword().testWord(password) ? isActive() && \res

0熱

1答えて

JMLの評価\ old（式[Id]）

\old(Expression[Id])という形式のJML式がどのように評価されているか、つまり\old(vector[value-1])式がある場合、\oldは「値」を参照するか、 vector[value-1]の値に設定します。前もって感謝します！

0熱

1答えて

JML、不変式の正確な定義

Javaモデリング言語の次の不変量に正確な意味を与えることができますか？公共不変抽象関数（プライベート不変）表現不変（プライベート不変）

2熱

1答えて

JMLの代替品

JMLのようなJava用の代替仕様言語オプションを探しています。誰も知っていますか？ありがとうございました。