Alloy 集合中的分析器元素比较

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)

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

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)（即 If 表达式 expr( x) 对于 x 的所有值都为真，则存在一个 x，其中 expr(x) 为真)

Answer 1

第一件事是你需要建模你的前，post-和操作。函数对此很糟糕，因为它们不能 not return 表示失败的东西。因此，您需要将操作建模为谓词。谓词的值指示是否满足 pre/post，参数和 return 值可以建模为参数。

据我了解你的操作：

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 中没有什么特别之处，它只是 post 状态的约定。我在这里稍微滥用它。

这已经足够 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 class，您从字面上理解了他：您的问题仍然基于 Ints。他的意思是不要使用 Int，不要把它们藏在地毯下。我理解 Daniel 的想法，但 Int 非常有吸引力，因为我们对他们非常熟悉。但是，如果你使用Int，至少让他们发挥出全部的光彩，不要隐藏起来。

希望这对您有所帮助。

以及整个模型：

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 }

Alloy 集合中的分析器元素比较

Alloy Analyzer element comparision from set

alloy

formal-verification