Pointwise effects¶
When an action modifies the value of a mutable field, one must usually specify how one part of the field is changed by the action, and how another part is left unchanged (as seen in the Behavioral modeling chapter, this part is called a frame condition). For instance, the action share associates a new sharing token t to file f, but other files are left unchanged by this operation.
pred share [f : File, t : Token] {
f in uploaded - trashed // guard
historically t not in File.shared // guard
shared' = shared + f->t // effect on shared
uploaded' = uploaded // no effect on uploaded
trashed' = trashed // no effect on trashed
}
In the specification above, the complete effect on relation shared, that is the modification part and the frame condition, is specified all at once by saying how the whole field, viewed as a binary relation, is to be updated. We call this style of effect purely relational or pointfree.
An alternative approach to the specification of effects is to rely on what we call a pointwise update. In this style, rather than specifying how shared evolves all at once, we make a distinction between the change for input file f specifically, and the frame condition for files other than f. This would result in the following alternative specification of share.
pred share [f : File, t : Token] {
f in uploaded - trashed // guard
historically t not in File.shared // guard
f.shared' = f.shared + t // effect on f.shared
all g : File - f | g.shared' = g.shared // no effect on other shared files
uploaded' = uploaded // no effect on uploaded
trashed' = trashed // no effect on trashed
}
The same style can be used for action predicates delete and download. Notice that the latter updates relation shared if token t is in its range. Nonetheless, the pointwise style can be used even if the join is performed on the right column of the relation.
pred delete [f : File] {
f in uploaded - trashed // guard
trashed' = trashed + f // effect on trashed
no f.shared' // effect on f.shared
all g : File - f | g.shared' = g.shared // no effect on other shared files
uploaded' = uploaded // no effect on uploaded
}
pred download [t : Token] {
some shared.t // guard
no shared'.t // effect on shared.t
all u : Token - t | shared'.u = shared.u // effect on other shared tokens
uploaded' = uploaded // no effect on uploaded
trashed' = trashed // no effect on trashed
}
Both styles are equivalent, so which one should you favor? Some people prefer the pointwise style because the modification of a field for a specific variable is arguably more salient. On the other hand, the relational style is shorter. Some people like this terseness because they can spot the effect of an action on a field in a single stroke. Ultimately, there are good arguments for both styles, so this is mainly a matter of personal taste!