pred 中的约束顺序是否重要？

Question

pred 中的约束顺序是否重要：

pred Example {
   A
   B
   C
}

A、B、C 表示约束。

那个pred和这个pred一样吗：

pred Example {
   B
   A
   C
}

if-then-else 中的约束是否有序？例如，ReadMemory 和 WriteMemory 是否在此 if-then-else 中排序：

pred Example {
    {
       ReadMemory
       WriteMemory
    } implies C else D
}

这是我提出问题的动机：Software Abstractions 的第 222 页有，This assertion says that if a read, write, load, and read are performed in that order, then ...

那句话中的“顺序”一词引起了我的注意。因此我的问题。

Answer 1

不，约束的顺序无关紧要。在你提到的例子中

 assert LoadNotObservable {
   all c, c’, c“: CacheSystem, a1, a2: Addr, d1, d2, d3: Data | 
    {read [c, a2, d2]
     write [c, c’, a1, d1]
     load [c’, c”] 
     read [c“, a2, d3] 
} implies d3 = (a1 = a2 => d1 else d2) } 

是参数 (c, c', c") 定义了转换的前后状态。