predの制約の順序は重要ですか？

Question

はこのpred問題で制約の順序ん：

pred Example { 
    A 
    B 
    C 
} 

A、B、Cは制約を表しています。

pred Example { 
    B 
    A 
    C 
} 

注文されたif-then-elseでの制約です：？

はpredこのpredと同じであることですかThis assertion says that if a read, write, load, and read are performed in that order, then ...

その文章中の単語 "順序" はキャッチ、Software Abstractionsの222を持っているページ：ここに私の質問の動機だ

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

：たとえば、ReadMemoryとWriteMemoryがIF-THEN-ELSEこの中で注文しています私の注意。したがって、私の質問です。

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 "）です言及。