Self-framing assertions
Assertions in Gobra must be well-defined.
This includes the fact that array indices in specifications must be in bounds.
Operations like division have conditions under which they are well-defined.
For a / b to be well-defined, b != 0 must hold.
In the context of permissions, we get a new requirement that assertions are self-framing,
i.e. access to all locations being read is required.
Gobra checks that assertions are self-framing, and reports an error otherwise.
This also applies to contracts.
In the following example, there is an error since *x and *y are accessed in the postcondition of swap,
without holding permissions for x and y:
ERROR Method contract is not well-formed.
Permission to *x might not suffice.
We can make it self-framing by returning the permissions acc(x) and acc(y):
Note that the order of the pre- and postconditions matters.
The contract is checked from top to bottom and permission must be held before accessing.
For example, if we exchange the postconditions of swap, we get the same error again:
ERROR Method contract is not well-formed.
Permission to *x might not suffice.
Conjunctions are evaluated from left to right. As a result,
is self-framing, while the following is not:
As an exception, the assertion from an assert statement must not be self-framing.
For example, we can write *x == 1 instead of acc(x) && *x == 1.
However, Gobra reports an error if acc(x) is not held in the state.
Well-defined assertions that require access to all locations being read are called self-framing. Gobra checks that assertions are self-framing, and reports an error otherwise.