Semantic of Multiple Assignments

[DavePearce]

An interesting question raised by @utting is what the real semantics for multiple assignments of the form x,y = e1,e2 are. For example, what about these statements:

x,x = x,y
a[i],a[j] = 1,2
*p, *q = 1,2

The question here is: what does it mean when the left-hand sides are not disjoint?

IDEA: One approach here is to require that they are disjoint. This would mean, for example, introducing proof obligations to establish that they are.

NOTES: The general assumption has been that the evaluation order follows left-to-right. Hence, all left-hand sides are evaluated first, then all right-hand sides and, finally, the assignment occurs (atomically).

[DavePearce]

Migrated from https://github.com/Whiley/WhileyCompiler/issues/879

[DavePearce]

An interesting observation regarding multiple assignments is the connection with type invariants. For example, consider this simple example:

type NonDiagonalPoint is { int x, int y } where x != y

function swap(NonDiagonalPoint p) -> (NonDiagonalPoint r):
    int tmp = p.x
    p.x = p.y
    p.y = tmp
    return p

Observe that this incorrectly verifies on whileylabs.com right now However, QuickCheck quickly identifies the potentially violated type invariant. Of course, we can easily fix this as follows:

function swap(NonDiagonalPoint p) -> (NonDiagonalPoint r):
    int p_x = p.x
    int p_y = p.y
    return {x:p_y,y:p_x}

But, an interesting question is whether or not this should be considered a valid implementation:

function swap(NonDiagonalPoint p) -> (NonDiagonalPoint r):
    p.x,p.y = p.y,p.x
    return p

This currently fails quick check, but it could easily be modified to accept this. For example, by only checking type invariants after the assignment statement has completed.

NOTE: regarding multiple assignments in this manner may be preferable from a performance perspective, such as when arrays are involved (i.e. to avoid copying the whole array).

[DavePearce]

The following except from 029_bipmatch illustrates one such scenario:

function match(Matching m, int from, int to) -> (Matching r)
// The target vertex cannot be matched; note, however,
// that the source vertex may already be matched
requires m.right[to] == UNMATCHED:
    //
    int l_from = m.left[from]
    //
    if l_from != UNMATCHED:
        // from was already matched
        m.right[l_from] = UNMATCHED
    //
    m.left[from] = to
    m.right[to] = from
    //
    return m

Here, there is a temporary breach of the type invariant for Matching at the assignment m.left[from] = to. I resolved this as follows

function match(Matching m, int from, int to) -> (Matching r)
// The target vertex cannot be matched; note, however,
// that the source vertex may already be matched
requires m.right[to] == UNMATCHED:
    //
    int[] m_left = m.left
    int[] m_right = m.right
    //
    int l_from = m_left[from]
    //
    if l_from != UNMATCHED:
        // from was already matched
        m_right[l_from] = UNMATCHED
    //
    m_left[from] = to
    m_right[to] = from
    //
    return { graph: m.graph, left: m_left, right: m_right }

[utting]

Dave

Yes, this is exactly why Boogie does not check ‘where’ clauses (type invariants) after each assignment statement. p30 of the Boogie Ref manual (KRML178) says:

Note that where clauses do not play a role for assignment statements. In particular, an assignment statement can set a variable to a value that does not satisfy its where clause. For example,

var volume : int where 0 6 volume ^ volume 6 10; x := 11;

sets volume to 11 , despite the fact that the where clause suggests volume is intended to be between 0 and 10. where clauses apply only in places where a variable gets an arbitrary value; by not applying them at assignment statements, Boogie provides the ability to use a sequence of statements that (perhaps temporarily) violates where conditions.

To explicitly say that a condition holds after an assignment, use an assume statement, as in:

Heap[this, C .data] := Heap[this, C .data] + 1; assume WellFormed(Heap);

So I’m pretty sure that in my translation, I have not currently got the semantics that you want for Whiley.

I agree that your swap example should be valid. And there may be a case for checking invariants even less frequently - e.g. just on return? But I don’t think this would work in Whiley - could lead to unsoundness...

Cheers Mark

[DavePearce]

Hey Mark,

Well, that is kinda interesting! Maybe for Boogie it makes sense to do that, but I don't think so for Whiley. In particular using nat times for loop counters is much nicer than having to write e.g. where i >= 0 all the time!!

[DavePearce]

Issue for WyC which may be relevant to this discussion.