問題タブ [formal-methods]

ご想像のとおり、ACL2 を使用してコードを証明する方法に関するリソースはたくさんありますが、証明済みのコードを運用環境で使用する方法に関するリソースはありません。

CLISP/Scheme/Clojure で動作するように ACL2 コードを微調整する必要がありますか? ACL2 も私のコードを実行できますか? （チュートリアルはどこにありますか、その目的に従ってではなく、ACL2を使用していますか？）

ありがとう！

このシナリオを単純化します (これは Perfect Developer にあり、すぐに複雑になります)。クラスに という単純なスキーマがあるとします。これは、(以前に定義されたクラス) をパラメーターとしてSucceed受け取ります。Course

基本的に、コースが前提条件として自分のコースにあることを確認してから、事後条件のセットにset追加します。coursesCompletedこの単純なスキーマはうまく機能し、次のようになります。

ただし、非常に単純なif条件を追加したいと思います。自分の courseCompleted カーディナリティが 30 以上の場合、Diplomation列挙型を " Ok" に設定します。カーディナリティが 30 未満の場合は、" NotOk"に設定します

Perfect Developer のドキュメント、および私が見たすべてのまれな例によると、if構文は次のようになります。

ただし、スキーマに直接プラグインすると、次のようになります。

それは機能しません、私はいつも「非常に説明的」になります

エラー！キーワード 'if' に構文エラーがあります。次のいずれかが必要です: '!' '(''?''c_address_of'

;どこにでも追加したり、 の後viaにキーワードを追加したり、post位置を変更したり、 と を交換したり;、,その他多くの試行錯誤を試みました。

私の質問は次のとおりです: ifPerfect Developer で、スキーマの事後条件に条件を追加するにはどうすればよいですか?

Perfect Developerでお答えください。私は（悲しいことに）自分の正式な方法を知っています。必要なのifは、世界で最悪のツールでコンパイルすることだけです。

以下を受け入れる操作 Bus_Arrives があります

LINE、BUS_ID、BUSROAD

• ある路線のバスが駅に到着し、空いているバス道路が割り当てられます。それ以外の場合はキューに入ります。

--------New_Bus_Arrives--------------------------------------------- -------------------------------------------------- ----

| | △バス停

| | バスライン?: LINE

| | バス?: BUS_ID

| | br?: バスロード

==============================================

| | 前提条件はこちら（それをキューに追加するケースは実装されていますが、質問とは関係ないので追加しません。） 以下は、この操作が完了した後のシステムの変化です。

| | free' = free \ {br?}

| | routing' = ルーティング

| | 出発' = 出発 U {br? |--> バス?}

| | 訪問数 = 訪問数 U {br? |--> ルーティング(|ライン?|) }

私の質問は次のとおりです。たとえば、訪問が正しく表現されている場合は Z です。たとえば、ルーティング (回線?) リレーションが呼び出されると、一連のステーション要素 {station1,station2,station3} が返されます。ただし、これを訪問関係にマッピングして更新するときは、次のようにしています: br? {station1,station2,station3} にマップされます。これは可能ですか、それとも br と言わなければなりませんか? セットのすべての要素に個別にマップされます。また、この場合、Z ではどのように表されますか?

説明内容に関する追加情報:

ルーティング: 対応するバス路線ごとに、バスがそこに到着するために通過する駅は何ですか (つまり、8 号線は LA、NY、マイアミに移動します)。

ルーティング: LINE <--> STATION (関係)

free: 利用可能なバス路線。

free: Π BUSROAD (パワーセット)

出発: すべてのバスがどのバス路線から出発するか (例: A がバス AY123 を出発)。

出発: LINE --> BUS_ID (機能)

訪問: 現在バスが割り当てられているすべてのバス道路について、どの駅を訪問するか。バス道路には、バスが 1 つだけある場合と、利用できる場合があります。

訪問: BUS_ROAD <--> STATION (関係)

event-b のラムダ式を1 つだけ使用して素数のシーケンスを生成できるかどうか疑問に思います。これは私がこれまでに持っているものです:

@axm1素数のセットを生成し@axm2、シーケンスのタイプを定義し、@axm3このセットをさらに決定論的な解に制約します。1つのラムダ式でこれを行う方法がわかりません。それが可能だとは思いませんが、他の人の考えを知りたいです。

ユーザー入力に応じて Alloy モデルを作成するスケーラブルなプログラムを Python で作成したいと考えています。特に、ユーザーにグラフを入力してもらい、Alloy を使用して、グラフにオイラー パスがあるかどうかをユーザーに伝えてもらいたいと考えています。グラフの特定のインスタンス用に Alloy でモデルを準備しました。ただし、Python コードで .als ファイルを生成し、Python で Alloy を起動してモデルを評価することを考えています。使用できる Alloy API や、特定の述語が一貫しているかどうかを判断するのに役立つコマンド ライン引数はありますか?

ありがとう

Alloyでバッグ(マルチセット)を使用してシステムをモデル化する方法はありますか? また、バッグの明確な概念がない場合、回避策はありますか?

ありがとう。