問題タブ [leon]

github の README.md ファイルから MacOSX (yosemite) 用の leon をビルドするための指示に従おうとしました。

基本的なテストを実行すると、scalaz3 ライブラリが見つからないという問題が発生することを除けば、うまくいきました。

Microsoft の Z3 (github から) をビルドする必要がある EPFL から ScalaZ3 パッケージをビルドしようとしました。z3 のビルド自体は機能しますが、ScalaZ3 のビルドは "gomp" ライブラリが見つからないため失敗します。

ここに MacOSX 用の Clang OMP ライブラリがあることがわかりました。

http://brewformulas.org

ただし、これには、clang-omp の brew のインストールを指すように、いくつかのビルド スクリプトを微調整する必要がある場合があります。

誰かが同様の問題を経験したり、解決したりしましたか?

• ニコラス。

scalac を直接使用して Leon コードをコンパイルしようとしています。残念ながら、コードが依存する Leon ライブラリを適切にビルドできませんでした。

たとえば、私は実行しました

しかし、これは実際にはエラーを返します:

ライブラリでこれらのエラーを回避し、最終的に自分のソース ファイルをコンパイルするには、scalac に何を渡す必要がありますか?

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

レオンと有理数で作業しているときに、次の問題に遭遇しました。inverse1関数の検証は反例を示しますが、inverse2検証中にはあまり意味がありません。

レオンが私に与える反例はこれです：

しかし、数学的に言えば意味がありません。

私はこのコードが==私が定義した演算子を呼び出すことを期待していましたが、これは常に返さtrueれ、関数は検証されないため、そうではないと考える傾向があります...

誰かがこのプログラムの何が問題なのか、または私の Scala/leon の理解を示すことができますか? ありがとう。

レオンで有理数に取り組んでいる間、isRationalほとんどどこでも要件として追加する必要があります。

例えば：

データ構造のすべてのインスタンスに適用されるように、クラス コンストラクターにステートメントを追加してrequireこのコードを DRY することは可能ですか? クラス本体の最初の行に追加してみましたが、効果がないようです...

Rational(0, 0)これは、レポートが示唆するように、レオンがたとえばを作成することを妨げません。

(また、常にコンストラクターの要件を満たしているthisとは限りません。)other

何か不足していますか？

ブール値を否定する次の複雑な方法を考えてみましょう (短絡評価に依存します)。

このコードを Scala コンソールでテストすると、期待どおりに動作します。しかしleon --xlang、事後条件が無効であると言います。これは期待/指定されていますか?

Leon の PropositionalLogic の例で、wrongCommutative のプロパティに非常に興味がありました。

私にとっては正しいプロパティのように思えますが、Leon でタイムアウトになる理由がわかりません。

ここにリンクがあります: https://leon.epfl.ch#link/37040293ff5ff92c763f797f22f142f8-1

誰でもこれで私を助けることができますか?

次のような抽象的なスタック型があります

pop最後にプッシュされた要素を返すことを確認したいと思います:

2 つの補題は同等ですが、Leon は 2 番目の補題の型パラメーターを識別できません。興味深いことに、Leon は Stackが具体的であっても非ジェネリックであっても問題ありません (例については、以下のリンクを参照してください)。これは Leon の機能ですか、それとも単なるバグですか?

完全なサンプル コードはここにあります。