合金分析仪元素对比

Question

一些背景知识：我的项目是制作一个从类 c 语言编译为 Alloy 的编译器。具有类似 c 语法的输入语言必须支持 contracts。目前，我正在尝试实现支持 pre 和 post condition 语句的 if 语句，类似于以下内容：

int x=2
if_preCondition(x>0)
if(x == 2){
   x = x + 1
}
if_postCondtion(x>0)

问题是我对合金的结果有点困惑。

sig  Number{
    arg1: Int,
}

fun addOneConditional (x : Int) : Number{
    { v : Number | 
            v.arg1 = ((x = 2 ) => x.add[1] else x)
    }
}

assert conditionalSome {
    all n: Number|  (n.arg1 = 2 ) => (some field: addOneConditional[n.arg1] | { field.arg1 = n.arg1.add[1] }) 
}

assert conditionalAll {
    all n: Number|  (n.arg1 = 2 ) => (all field: addOneConditional[n.arg1] | { field.arg1 = n.arg1.add[1] }) 
}

check conditionalSome
check conditionalAll

在上面的例子中，conditionalAll 不会生成任何Counterexample。但是，conditionalSome会生成Counterexamples。如果我正确理解 all 和 some 量词，那么就有错误了。因为从数学逻辑我们有 Ɐx expr(x) => ∃x expr(x) （即如果表达式 expr(x) 对所有值都为真x 那么存在一个 x 且 expr(x) 为真)

Answer 1

第一件事是您需要建模您的前期、后期和操作。函数对此很糟糕，因为它们不能不返回表明失败的东西。因此，您需要将操作建模为谓词。谓词的值表示是否满足前/后，参数和返回值可以建模为参数。

据我所知你的操作是这样的：

pred add[ x : Int, x' : Int ] {
  x > 0             -- pre condition
  x = 2 => 
    x'=x.plus[1] 
  else 
    x'=x
  x' > 0            -- post condition
}

Alloy 没有可写变量（Electrum 有），因此您需要使用 prime (') 字符对前后状态进行建模。

我们现在可以使用这个谓词来计算您的问题的解决方案集合：

fun solutions : set Int {
  { x' : Int | some x : Int | add[ x,x' ] }
}

我们用整数创建一个集合，我们有一个结果。主字符在 Alloy 中没有什么特别之处，它只是后状态的约定。我在这里稍微滥用它。

这已经足够Alloy来源犯错误了，所以让我们测试一下。

run { some solutions }

如果你运行它，你会在Txt 视图中看到：

skolem $solutions={1, 3, 4, 5, 6, 7}

这符合预期。 add 操作仅适用于正数。 检查。如果输入为 2，则结果为 3。因此，2 永远不可能是解。 检查。

我承认，我对您在断言中所做的事情感到有些困惑。我试图忠实地复制它们，虽然我已经删除了不必要的东西，至少我认为我们是不必要的。首先是您的some 案例。您的代码正在执行all，但随后选择了 2。因此删除了外部量化并硬编码了 2。

check  somen {
    some x' : solutions | 2.plus[1] = x'
}

这确实没有给我们任何反例。因为solutions是{1, 3, 4, 5, 6, 7}，所以2+1=3在集合中，即满足some条件。

check  alln {
    all x' : solutions  | 2.plus[1] = x'
}

但是，并非所有解决方案都以 3 作为答案。如果你检查这个，我会得到以下反例：

skolem $alln_x'={7}
skolem $solutions={1, 3, 4, 5, 6, 7}

结论。 Daniel Jackson 建议不要用 Ints 学习 Alloy。看着您的 Number 课程，您从字面上理解了他：您仍然将问题基于 Ints。他的意思是不要使用 Int，不要将它们隐藏在田野的地毯下。我知道 Dan​​iel 来自哪里，但 Ints 非常有吸引力，因为我们对它们非常熟悉。但是，如果你使用 Ints，至少要让它们充分发挥它们的光彩，不要隐藏它们。

希望这会有所帮助。

还有整个模型：

pred add[ x : Int, x' : Int ] {
    x > 0               -- pre condition
    x = 2 => 
        x'=x.plus[1] 
    else 
        x'=x
    x' > 0              -- post condition
}   
fun solutions : set Int { { x' : Int | some x : Int | add[ x,x' ] } }

run { some solutions }
check  somen { some x' : solutions | x' = 3 }   
check  alln { all x' : solutions  | x' = 3 }