問題タブ [openjml]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
java - 実数についての推論
Z3 と組み合わせて OpenJML を試しており、次の値について推論しようとしていdoubleますfloat。
OpenJML がAUFLIAをサポートしていないデフォルトのロジックとして使用していることはすでにわかっていますreals。私は今使用してAUFNIRAいます。
残念ながら、ツールはこのクラスを証明できません:
どうしてこれなの？
java - openJML を使用してマトリックスを反復処理する
特定の位置にすべて 0 と 1 で初期化されたマトリックスを持つクラスがあります。
不変条件を追加して、値が 1 の 1 セルと値が 0 の 35 セルが常に 1 つしかないことを確認したいと思います。
しかし、コンストラクタの直後に不変エラーが発生します。プロパティをチェックするためにマトリックスを反復処理するにはどうすればよいですか?
java - Maven ビルドでの契約チェック
私は IJ で Java コードベースに取り組んでおり、現在 Maven で構築しています。コードの一部を、Maven ビルドで取り上げられる何らかの形式のコントラクトで補足したいと思います。これまでのところ、私はそのような機能を既製品で探すことに成功していません。
- OpenJMLですが、コードを分析するには独自のツールが必要なようで、ビルドに簡単に統合する方法が見つかりませんでした。
- Jetbrains 契約。これらはインスペクションを介して IntelliJ で警告を発しますが、ビルドには影響しません。
注:ここでは、コンパイル時にチェック可能なコントラクトのみを扱います。ランタイム側でスローするJUnitがあります。
実施する契約:
このセクションを追加して、どのような種類の契約を施行したいかというコメントに答えました。理想的には、そのソリューションが完全であることを条件として、可能な限り最も強力なソリューションを希望します。ここで完全とは、言語のすべてのステートメントがコンパイル時にチェッカーによって良いか悪いかをチェックできるような、コントラクトの言語とコントラクト チェッカーを意味します。これは大きな質問かもしれませんが、Jetbrains が提供するものなど、最も単純な契約でも満足します。
具体的な例として、次の関数を検討してください。
これにより、Jetbrains コントラクトが正常に通過します。
そして、この不自然な契約は失敗します:
しかし、上記の不自然で悪いコントラクトを使用しても、Maven ビルドは問題なく動作します。ビルドは検査結果を取得しません。これらは IJ 内からのみ表示されます。ビルドにフックして、契約に違反した場合に失敗できるようにしたいと思います。