来自集合的合金分析仪元素比较

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量词，那么可能是一个错误。因为根据数学逻辑，我们有Ɐxexpr（x）=>∃xexpr（x）] >>（即如果表达式expr（x）对于x的所有值都是true，则存在一个x对于expr（x）为true）

某些背景：我的项目是制作一个从类似c的语言编译为Alloy的编译器。具有类似c语法的输入语言必须支持合同。现在，我正在尝试实现...

Answer 1

第一件事是，您需要模型