什么时候约束是隐式与的，什么时候约束必须是显式的？

Question

此签名包含两个字段，每个字段都包含一个整数：

sig Test {
    a: Int,
    b: Int
}

这个谓词包含一系列约束：

pred Show (t: Test) {
    t.a = 0
    t.b = 1
}

这些约束被隐式地“与”在一起。所以，那个谓词等价于这个谓词：

pred Show (t: Test) {
    t.a = 0 and
    t.b = 1
}

此断言包含一系列约束，后跟一个蕴涵运算符：

assert ImplicationTest {
    all t: Test {
        t.a = 0
        t.b = 1 => plus[t.a, t.b] = t.b
    }
}

但在这种情况下，约束并没有隐式地与在一起。如果我想将它们与在一起，我必须明确地与它们：

assert ImplicationTest {
    all t: Test {
        t.a = 0 and
        t.b = 1 => plus[t.a, t.b] = t.b
    }
}

这是为什么？为什么有时一系列约束被隐式地与在一起，而其他时候我必须显式地与约束？

Answer 1

我查看了解析器，据我所知，它将换行符/空格的右侧和左侧视为带括号的表达式。

expr exprs -> expr and exprs

因此：

t.a = 0  t.b = 1   t.c =2  => plus[t.a, t.b] = t.b

相当于：

(t.a = 0) and (t.b = 1 and ( t.c => plus[t.a, t.b] = t.b))

以下模型似乎证明了这些表达式是等价的：

sig Test {
    a: Int,
    b: Int,
    c: Int
}

pred simple( t: Test ) {
    t.a = 0 t.b = 1 t.c = 2 => plus[t.a, t.b] = t.b
}

pred full( t: Test ) {
    (t.a = 0) and  ((t.b = 1) and (t.c=2 => plus[t.a, t.b] = t.b))
}

assert Equivalent {
    all t : Test {
        simple[t] <=> full[t]
    }
}

check Equivalent for 10