找到实例

Question

是否有可能搜索的谓词执行（谓语应用程序序列），从给定的状态导致另一个约束状态的实例？

一个有点相关的问题：有没有办法通过一个谓语参数另一个谓词？

Answer 1

这不是完全清楚你在找什么，至少对像我这样的读者谁认为谓词的事情评估，不事执行。

是否有可能搜索的谓词执行情况下...？

听起来好像在这里你正在寻找在2.4节“执行跟踪”和其他地方在杰克逊的软件抽象讨论之类的话（见指数“跟踪”）。的基本思想是

• 限定描述的初始状态的谓词（杰克逊的示例调用它INIT）
• 定义一组描述可能从一个状态转变到状态谓词
• 强加的总体排序上各州

• 定义谓词用于检查执行迹线大致需要形式

  pred traces { 
      init [first] /* 'first' is defined by util/ordering[State] */ 
      all s : State - last 
      | let s' = next[s] 
      | Possible_Transition[s, s'] 
  } 
  

许多变化当然是可能的。

有没有办法将谓词作为参数传递给另一个谓词？

没有，是的。

否，因为Alloy使用一阶逻辑;谓词的所有参数都是延伸定义的原子集合。

是因为过程中的一个可以制作一个映射1的签名具体化谓词：1的组谓词，并通过每当周围人想传递一个谓词签名的原子。鉴于人们希望以这种方式来表达的有限数量的谓词，这总是可能的。 （请原谅我，如果这点和下面的解释是crashingly明显给你;我还记得的时候，他们没有crashingly明显，我，我希望堆栈溢出，一些读者对他们来说，他们不是很明显。）

假设我们有两个谓词P和Q，其中每一个取Atom类型的原子论点a。我们希望定义一个元谓语M，它接受原子x和谓词Y并返回值Y[x]。

// First some scaffolding 
sig Atom {} 
pred P [a : Atom] { ... // whatever you like } 
pred Q [a : Atom] { ... // whatever ... } 

// Now the heart of the matter 
abstract sig reification {} 
one sig p, q extends reification {} 

pred M [x : Atom, Y : reification] { 
    (Y = p) implies P[x] 
    else (Y = q) implies Q[x] 
    else x != x 
} 

取决于你为什么要传递谓词作为参数，你可以振振有词地采取这样的一种方式来做到这一点，或者为什么您可能不希望做这样一个示范。如果高阶谓词是你想要考虑的重要部分，像Alloy这样的一阶系统可能不是最好的匹配。

但是像其他一阶系统一样，Alloy可以用一些谨慎和努力来支持更高阶的参数。当我们应用合金来表明给定的设计具有属性P时，我们最常见的情况是支持所有设计的正确实现都将具有属性P的声明，这种声明在Alloy中可能采取all i : Implementation | correctly_implements_design[i] implies has_property_P[i]的形式。但是一个实现（略微简化）输入和输出之间的关系。所以关于实现的任何陈述都是二阶索赔。因此，在推广给定设计的所有实现时，我们正在制作一阶参数（以Alloy模型表示）以支持二阶索赔。

如果您对使用Alloy对二阶命题进行争论有着浓厚的兴趣，您可以参考Jackson的书中的3.2.3,5.2.2和5.3节。