Syntax for Framing

[DavePearce]

(see also #39 and #38)

Currently, there is no mechanism for framing in Whiley. That is describing what locations can be modified. There are several different approaches here:

• Set Generator. Dafny employs an approach based around using sets to describe modified locations. This is quite powerful.
• Mutable References. Rust provides mutable references to clarify what can and cannot be modified. In particular, nothing can be modified through an immutable reference.
• Variance Types. Another approach is to provide a mechanism for describing how types are permitted to change. This could connect with other requirements around concurrency (#25, #31, #45, #46).

Papers

1. Implicit Dynamic Frames, TOPLAS'12 [PDF]
2. Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic, ECOOP'09. [PDF]
3. The Relationship between Implicit Dynamic Frames and Separation Logic, LMCS'12 [PDF]

[DavePearce]

@utting this is as far as I’ve got thinking about thia...

[DavePearce]

One thing that is apparent to me (and mentioned in the TOPLAS paper above), is that you can infer framing from a method's specification. For example, consider this (using syntax from RFC#84:

method swap(&int x, &int y)
ensures *x == 'y && *y == 'x:
    ...

In particular, an occurrence of *x in the post-condition implies that it must be read, whilst an occurrence of 'x implies it must be written. In this way we can infer a suitable framing condition for swap(). However, in general, we will want implementations to be hidden and, hence, a given specification will not necessarily indicate all locations that are modified.