Utiliser des prédicats dans Alloy

Question

J'essaie d'utiliser deux prédicats (par exemple, METHODSWiThSameParameters et METHODSWiThSameReturn) à partir d'un autre (c'est-à-direcheckOverriding) mais je reçois l'erreur suivante :"Il n'y a aucune commande à exécuter".Des indices ?J'ai également essayé d'utiliser des fonctions mais sans succès, soit à cause de la syntaxe, soit parce que les fonctions ne renvoient pas de valeurs booléennes.

Ils font partie d'un métamodèle Java spécifié dans Alloy, comme je l'ai commenté dans certaines questions précédentes.

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

---

Merci pour votre réponse, monsieur C.M.Sperberg-McQueen, mais je pense que je n'ai pas été assez clair dans ma question.

Mon prédicat, disons checkOverriding, est appelé à partir d'un fait comme celui-ci :

fact chackJavaWellFormednessRules{
    checkOverriding[]
}

Ainsi, je continue de ne pas comprendre l'erreur :"Il n'y a aucune commande à exécuter" .

Answer 1

Vous avez défini des prédicats ;ils ont une sémantique purement déclarative et ils seront vrais dans certains sous-ensembles d'instances du modèle et faux dans le sous-ensemble complémentaire.

Si vous souhaitez que l'analyseur fasse quelque chose, vous devez lui donner une instruction ;l'instruction pour rechercher une instance d'un prédicat est run.Alors tu auras envie de dire quelque chose comme

run methodsWithSameParameters for 3

ou

run methodsWithSameParameters for 5
run methodsWithSameReturn for 5

Notez que vous pouvez avoir plusieurs instructions dans un modèle Alloy ;l'analyseur vous permet de lui indiquer lequel exécuter.

---

[Addenda]

L'analyseur d'alliage concerne les mots-clés run et check (et seulement eux) en tant que « commandes ».D'après votre description, il semble que vous n'ayez aucune occurrence de ces mots-clés dans le modèle.

Si tout ce que vous voulez faire est de voir quelques instances du modèle Alloy (pour vérifier que le modèle n'est pas contradictoire), alors le moyen le plus simple est d'ajouter quelque chose comme ce qui suit au modèle :

pred show {}
run show for 3

Ou, si vous avez déjà un prédicat nommé, vous pouvez simplement ajouter un run commande pour ce prédicat :

run checkOverriding 

Mais sans clause dans le modèle commençant par l'un ou l'autre run ou check, vous n'avez pas de « commande » dans le modèle.

Vous dites que vous avez défini un prédicat (checkOverriding) puis précisé dans un fait que ce prédicat est toujours satisfait.Cela revient à dire que le prédicat checkOverriding est toujours vrai (et pourrait tout aussi bien être fait en faisant checkOverriding un fait au lieu d'un prédicat), mais il a un sens purement déclaratif et ne compte pas comme un « ordre ».Si vous souhaitez qu'Alloy trouve des instances d'un prédicat, vous devez utiliser l'option run commande;si vous voulez qu'Alloy trouve des contre-exemples pour une assertion, vous devez utiliser le check commande.