Usando i predicati in lega

Question

Sto cercando di utilizzare due predicati (diciamo, metodoswithsameparameters e metodyswithSamereTurn) da un altro (cioè checkoverriding) ma ricevo il seguente errore: "Non ci sono comandi da eseguire".Qualche indizio? Ho anche provato a utilizzare le funzioni ma senza successo, a causa della sintassi o delle funzioni non restituire valori booleani.

fanno parte di un metamodello Java specificato in lega, come ho commentato in alcune domande precedenti.

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

.

---

.

Grazie per la tua risposta, signor C. M. Sperberg-McQueen, ma penso di non essere abbastanza chiaro nella mia domanda.

Il mio predicato, ad esempio checkoverriding, viene chiamato da un fatto come questo:

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

.

Quindi, continuo a non capire l'errore: "Non ci sono comandi da eseguire".

Answer 1

hai definito i predicati; Hanno una semantica puramente dichiarativa e saranno vere in alcuni sottoinsieme di istanze del modello e false nel sottoinsieme complementare.

Se vuoi che l'analizzatore faccia qualsiasi cosa, è necessario dargli un'istruzione; Le istruzioni per la ricerca di un'istanza di un predicato è run. Quindi vorrai dire qualcosa come

run methodsWithSameParameters for 3

.

o

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

.

Nota che è possibile avere più di un'istruzione in un modello in lega; L'analizzatore ti consente di dire che da eseguire.

---

.

[Addendum]

L'analizzatore in lega riguarda le parole chiave run e check (e solo loro) come "comandi". Dalla tua descrizione, suona molto come se non si disponga di alcuna occasione di quelle parole chiave nel modello.

Se tutto ciò che vuoi fare è vedere alcuni istanze del modello in lega (per verificare che il modello non sia auto-contraddittorio), allora il modo più semplice è aggiungere qualcosa come il seguente al modello:

pred show {}
run show for 3

.

O, se hai già un predicato denominato, puoi semplicemente aggiungere un comando run per quel predicato:

run checkOverriding 

.

Ma senza una clausola nel modello che inizia con run o check, non si dispone di un 'comando' nel modello.

Dici che hai definito un predicato (checkOverriding) e quindi specificato in un fatto che il predicato è sempre soddisfatto. Ciò equivale a dire che il predicato checkOverriding è sempre vero (e potrebbe anche essere fatto rendendo checkOverriding un fatto invece di un predicato), ma ha un significato puramente dichiarativo, e non conta come un "comando". Se si desidera che le lega trovi le istanze di un predicato, è necessario utilizzare il comando run; Se si desidera che le lega trovi contro-esemplari per un'asserzione, è necessario utilizzare il comando check.