当隐含的约束与AND运算时，必须限制明确相与？

Question

该签名包含两个字段，每个保持的整数：

sig Test { 
    a: Int, 
    b: Int 
} 

该断言包含一系列约束：

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

这些约束被隐式AND关系结合在一起。所以，这谓词相当于这个谓词：

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 
    } 
} 

但是，在这种情况下，约束不是隐含AND关系结合在一起。如果我要他们AND'ED在一起，我必须明确地与他们：

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

这是为什么？为什么有时一系列的限制条件都隐含AND关系结合在一起，而其他时间我必须明确地和限制？

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