The Armada language doesn't offer a way to describe the conditions under which a certain expression is well-formed. It would be useful to have $wf(E) mean "the expression E is well-formed". For instance, $wf(n/d) would be equivalent to d != 0, and $wf(p + 7) where p is a pointer would be equivalent to "p is a pointer into an array that has at least seven more elements in it beyond p".
Currently, if the developer writes an inductive invariant or yield predicate that isn't always well-formed, we automatically add extra conditions to ensure it's well-formed. For instance, if the developer writes n/d == 3 as an invariant we transform it to d != 0 && n/d == 3. This may be surprising to developers since the invariant we generate doesn't exactly match what they wrote. Providing $wf
in the language might remove the need to change invariants this way.
The Armada language doesn't offer a way to describe the conditions under which a certain expression is well-formed. It would be useful to have $wf(E) mean "the expression E is well-formed". For instance, $wf(n/d) would be equivalent to d != 0, and $wf(p + 7) where p is a pointer would be equivalent to "p is a pointer into an array that has at least seven more elements in it beyond p".
Currently, if the developer writes an inductive invariant or yield predicate that isn't always well-formed, we automatically add extra conditions to ensure it's well-formed. For instance, if the developer writes n/d == 3 as an invariant we transform it to d != 0 && n/d == 3. This may be surprising to developers since the invariant we generate doesn't exactly match what they wrote. Providing $wf in the language might remove the need to change invariants this way.