問題タブ [formal-methods]

KeYの強みを示すコード例は何ですか?

詳細

非常に多くの Formal Method ツールが利用できる中で、KeY が競合他社よりも優れている点はどこでしょうか? いくつかの読みやすいコード例は、比較と理解に非常に役立ちます。

アップデート

KeY の Web サイトを検索すると、本からコード例が見つかりました。適切なコード例がどこかにありますか?

さらに、KeY さんが Java 8 の mergeCollapse in TimSort で見つけたバグに関する論文を見つけました。KeY の強みを示す TimSort の最小限のコードは何ですか? ただし、モデル チェックでバグを検出できないと思われる理由がわかりません。64 要素のビット配列は大きすぎて処理できません。他の演繹的検証ツールでもバグを見つけることができますか?

適切なコード例を使用した確立された検証コンペティションはありますか?

TLA での私の理解では、最終的なアクション (<>) は、次の状態でスタッターが発生することを許可していません。では、次の状態変数は、無限に頻繁 ([]<>) の場合、吃音を許可しないということですか?

気象条件の例を挙げると、無限に多くの場合、最終的には年に何日も雨が降る (いつ起こるかはわかりません) と説明できますが、雨が降った日の後に天気は晴れでなければなりませんか?

無限に対する私の理解は正しいですか？私が間違っている場合は修正してください。

ありがとうございました。

数値変数とブール変数の間の関係をモデル化しようとしています。数値変数が特定の範囲内にある場合、ブール変数は値を変更します。私は合金を初めて使用し、明らかな反例を生成するのに十分な範囲を制限する方法を理解するのに苦労しています。私のコードは次のとおりです。

o.integerは整数値であり、範囲は 0 から 10 であるため、10 の異なる選択肢のうちの 1 つにすぎません。そして、それぞれが oneと oneObjectのみを持つように指定しました。したがって、ここでチェックするケースは実際には 10 個しかないというのが理にかなっているように思えます。それでも、1000ケースでも、integerdiscreteinteger

反例は見つかりませんでした。

変数と関連する事実を削除するintegerと、反例がすぐに見つかります。また、他のソルバーを使用して、オプションでさまざまな深度とメモリの値を増やしてみましたが、これは役に立ちませんでした。明らかに私のコードに問題があります。

Alloy が反例を見つけられるようにスコープを制限するにはどうすればよいですか ( の可能な値を反復処理することによってinteger)? ありがとう！

完全な開示、これは大学のコース用です。私は完全な答えを期待していませんが、助けていただければ幸いです。

Z 表記を使用して Item エンティティをモデル化する必要があります。これは説明です：

アイテム: すべてのアイテムには、アイテムを一意に説明するために使用できる名前と一意の ID があります。アイテムには、価格 (正のフロート) とカテゴリもあります。

要件の一部は、量指定子なしでこれらのエンティティをモデル化することです。

これは私が最終的に得たものですが、それが正しいかどうかはわかりません:

アイテムのスキーマ

名前は文字列の組み合わせであり、ID は正の整数とその名前のタプルであり、価格とカテゴリの両方が合計関数でマッピングされるという考えです。

最初の述語は正の価格を確保するためのもので、2 つ目は ID の一意性を確保するためのものです。つまり、ドメインをまだ割り当てられていないすべての整数に減らします。これが正しいとは思いませんが。

forallRuby や JavaScript などの手続き型言語または OO 言語で実装する方法を理解しようとしています。例（これはCoqです）：

これを行う私の試みは、このようなクラスを定義するだけです (call MainAxiom == ax)。

これにはあらゆる種類の間違いがあります。基本的に、「点p1とp2で作成するすべての公理について、線上にあるなどのプロパティを満たさなければならない..」と言っていますが、これは私がやりたいことではありません。実際の公理を定義するという数学的目標を達成したいと考えています。

Ruby や JavaScript などの言語でこれを実現する方法を知りたいのですが、それが直接可能でない場合は、可能な限り近いものを作成してください。それが単なる DSL やデータを定義するオブジェクトであっても、代わりの方法を知っておくと役に立ちます。

最初に気になったのは、attr :p1and attr の定義がすべてのインスタンスに適用されるように見えるということです。つまり、forallについて何かを言っているように見えますが、特定することはできません。

たぶん、これにもっと近いものがあります：

forall手続き型/オブジェクト指向言語の定義に半分でも近いものが欲しいだけです。