Verwendung von Prädikaten in Alloy

Question

Ich versuche, zwei Prädikate (z. B. „methodsWiThSameParameters“ und „methodsWiThSameReturn“) von einem anderen zu verwenden (z. B.checkOverriding), aber ich erhalte die folgende Fehlermeldung:„Es sind keine Befehle zum Ausführen vorhanden.“Irgendwelche Hinweise?Ich habe auch versucht, Funktionen zu verwenden, aber ohne Erfolg, entweder aufgrund der Syntax oder weil Funktionen keine booleschen Werte zurückgeben.

Sie sind Teil eines in Alloy spezifizierten Java-Metamodells, wie ich in einigen früheren Fragen kommentiert habe.

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) 
}

---

Vielen Dank für Ihre Antwort, Herr C.M.Sperberg-McQueen, aber ich glaube, ich habe mich in meiner Frage nicht klar genug ausgedrückt.

Mein Prädikat, sagen wir checkOverriding, wird von einer Tatsache wie dieser aufgerufen:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

Daher verstehe ich den Fehler weiterhin nicht:„Es sind keine Befehle zum Ausführen vorhanden.“

Answer 1

Sie haben Prädikate definiert;Sie haben eine rein deklarative Semantik und sind in einigen Teilmengen von Instanzen des Modells wahr und in der komplementären Teilmenge falsch.

Wenn Sie möchten, dass der Analysator etwas tut, müssen Sie ihm eine Anweisung geben;Die Anweisung, nach einer Instanz eines Prädikats zu suchen, lautet run.Sie möchten also etwas sagen wie

run methodsWithSameParameters for 3

oder

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

Beachten Sie, dass Sie in einem Legierungsmodell mehr als eine Anweisung haben können.Mit dem Analysator können Sie festlegen, was ausgeführt werden soll.

---

[Nachtrag]

Der Legierungsanalysator berücksichtigt die Schlüsselwörter run Und check (und nur sie) als „Befehle“.Aus Ihrer Beschreibung geht hervor, dass diese Schlüsselwörter im Modell nicht vorkommen.

Wenn Sie lediglich einige Instanzen des Alloy-Modells sehen möchten (um zu überprüfen, ob das Modell nicht widersprüchlich ist), dann ist es am einfachsten, dem Modell etwas wie Folgendes hinzuzufügen:

pred show {}
run show for 3

Wenn Sie bereits ein benanntes Prädikat haben, können Sie einfach ein hinzufügen run Befehl für dieses Prädikat:

run checkOverriding 

Aber ohne eine Klausel im Modell, die mit einem von beiden beginnt run oder check, Sie haben keinen „Befehl“ im Modell.

Sie sagen, dass Sie ein Prädikat definiert haben (checkOverriding) und dann in einer Tatsache angegeben, dass dieses Prädikat immer erfüllt ist.Dies läuft darauf hinaus zu sagen, dass das Prädikat checkOverriding ist immer wahr (und könnte genauso gut dadurch erreicht werden, dass man checkOverriding eine Tatsache statt eines Prädikats), hat aber eine rein deklarative Bedeutung und zählt nicht als „Befehl“.Wenn Sie möchten, dass Alloy Instanzen eines Prädikats findet, müssen Sie die verwenden run Befehl;Wenn Sie möchten, dass Alloy Gegenbeispiele für eine Behauptung findet, müssen Sie die verwenden check Befehl.