CODEWITHSUNDEEP
alloy
Roger Costello
Roger Costello

Reputation: 3209

Does the order of constraints in a pred matter?

Does the order of constraints in this pred matter:

pred Example {
   A
   B
   C
}

A, B, C represent constraints.

Is that pred the same as this pred:

pred Example {
   B
   A
   C
}

Are the constraints in an if-then-else ordered? For example, is ReadMemory and WriteMemory ordered in this if-then-else:

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

Here's the motivation for my question: Page 222 of Software Abstractions has, This assertion says that if a read, write, load, and read are performed in that order, then ...

The word "order" in that sentence caught my attention. Hence my question.

Upvotes: 1

Views: 88

Answers (1)

Daniel Jackson
Daniel Jackson

Reputation: 2768

No, order of constraints does not matter. In the example you mention

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

it's the parameters (c, c', c") that define the pre and post states for the transitions.

Upvotes: 2

Related Questions