主页 / coding / 问题 / 78529388
Accepted
luomein
Asked: 2024-05-24 23:07:51 +0800 CST

Alloy 接受自由变量吗？

  • 772

在《Software Abstractions》一书中，第 5.2.2 Skolemization 章提到， 在此输入图像描述

其中sx是新的自由变量F[sx/x]是约束F，用sx代替x。

但是，当我在 Alloy 中提供自由变量时，它显示语法错误。Alloy 接受自由变量吗？

sig A {
  relation:  A
}
fact {
 some A
}
check{
  //correct expression
  //some a : A | one a.relation

  //Skolemization
  (a: A) and (one a.relation)
}
alloy

1 个回答

  1. Best Answer

    首先，Skolemization 是一种经典的逻辑运算，如果您还不知道它，那么使用逻辑书籍来学习它也许是个好主意。

    话虽这么说，书中提到的约束不是有效的 Alloy 代码，而是对求解器级别发生的情况的解释（杰克逊称之为“分析约束”）。所以，不，这样写，由于存在这个自由变量，模型不是有效的 Alloy。

    但是，您不必自己执行 Skolemization，因为 Alloy 会为您执行（取决于“选项”菜单中的配置）。

    不过，如果你愿意，你也可以。方法是为存在变量添加一个新的a类型对象，如下所示：A

    sig A {
  relation:  A
}
fact {
  some A
}
one sig a in A {}
check{ one a.relation }
    • 1

相关问题