合金の述語を使用する

Question

私は別のもの（すなわちCheckoVerriding）から2つの述語（つまり、CheckoVerriding）から2つの述語を使用しようとしていますが、次のエラーが表示されます。「実行するコマンドはありません」。手がかり？ また、機能を使用しようとしましたが、構文や関数のどちらかで、ブール値を返しません。

彼らは、私がいくつかの以前の質問でコメントしたように、合金で指定されたJavaメタモデルの一部です。

pred checkOverriding[]{
//check accessibility of methods involved in overriding
  no c1, c2: Class {
    c1=c2.^extend
    some m1, m2:Method |
          m1 in c1.methods && m2 in c2.methods && m1.id = m2.id 
          && methodsWiThSameParameters[m1, m2] && methodsWiThSameReturn[m1, m2] && 
               ( (m1.acc = protected && (m2.acc = private_ || #(m2.acc) = 0 )) ||
                 (m1.acc = public && (m2.acc != public || #(m2.acc) = 0 )) ||
                 (#(m1.acc) = 0 && m2.acc != private_ )
               )
      }
    }

pred methodsWiThSameParameters [first,second:Method]{
    m1.param=m2.param || (#(m1.param)=0 && #(m2.param)=0)  
}
pred methodsWiThSameReturn [first, second:Method]{
    m1.return=m2.return || (#(m1.return)=0 && #(m2.return)=0) 
}

.

---

あなたの反応をありがとう、C. M. Sperberg-McQueen氏ですが、私は私の質問では十分明確ではなかったと思います。

私の述語、CheckoVeridingは、このような事実から呼ばれています。

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

.

したがって、私はエラーを理解していません： "実行するコマンドはありません"。

Answer 1

述語を定義しました。それらは純粋に宣言的な意味論を持っていて、それらはモデルのインスタンスのサブセットと相補的なサブセットでの偽のいくつかのサブセットで真実です。

アナライザーに何もしたい場合は、命令を入力する必要があります。述語のインスタンスを検索する命令はrunです。だからあなたは

のようなことを言いたいです

run methodsWithSameParameters for 3

.

または

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

.

合金モデルで複数の命令を持つことができることに注意してください。アナライザを使用すると、実行先を教えてください。

---

[補遺]

合金アナライザは、キーワードrunとcheck（そしてそれらのみ）を 'コマンド'と見なします。あなたの説明から、モデル内のそれらのキーワードが発生していないかのようにそれは非常に聞こえます。

あなたが何をしたいのなら、合金モデルのいくつかのインスタンスを見ることは（モデルが自己矛盾でないことを確認するために）、最も簡単な方法はモデルに次のようなものを追加することです：

pred show {}
run show for 3

.

または既に名前付き述語をお持ちの場合は、その述語のrunコマンドを単純に追加することができます。

run checkOverriding 

.

しかしrunまたはcheckで始まるモデルの句を指定しないで、モデルに 'コマンド'がありません。

述語（checkOverriding）を定義し、その述語が常に満たされているという事実で指定されたと言います。これは、述語checkOverridingが常に真になると言うことになります（そして述語の代わりにcheckOverridingを事実を事実にすることによって行われるかもしれません）が純粋に宣言的な意味を持ち、 "コマンド"としてカウントされません。合金が述語のインスタンスを見つけたい場合は、runコマンドを使用する必要があります。アロイがアサーションのカウンタ例を見つけるようにしたい場合は、checkコマンドを使用する必要があります。