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「）。