type Node is { int data }
type Link is null | Node
function f(Link[] ls))
requires some { i in 0..|ls| | ls[i] is Node && ls[i].data >= 0 }
(this is an artificial example, but it serves the point)
The problem is that this cannot type check! The current work around is to do this:
property validNode(Link ls)
where (ls is Node) && (ls.data >= 0)
function f(Link[] ls))
requires some { i in 0..|ls| | validNode(ls) }
However, this is a bit ugly, let's face it. There are at least two possible solutions:
(Flow Typing of Arrays) Allow flow typing of arrays in expressions (because they are immutable). Therefore, can retype ls[i] in the original example above.
(Expression Let Syntax) Allow some kind of let-expression (e.g. let l = ls[i] in (l is Node) && (l.data >= 0))
To be honest, we probably want both! Also, the general logic here applies to both references and functions. Furthermore, we could extend it beyond expressions by allowing it up to invalidation. For example:
function f(Link[] ls, int i):
if ls[i] is Node:
Node n = ls[i]
...
This should be safe since nothing has invalidated ls[i]. Specifically, any assignment to ls would invalidate it.
Recently, a situation like the following arose:
(this is an artificial example, but it serves the point)
The problem is that this cannot type check! The current work around is to do this:
However, this is a bit ugly, let's face it. There are at least two possible solutions:
ls[i]in the original example above.let l = ls[i] in (l is Node) && (l.data >= 0))To be honest, we probably want both! Also, the general logic here applies to both
referencesandfunctions. Furthermore, we could extend it beyond expressions by allowing it up to invalidation. For example:This should be safe since nothing has invalidated
ls[i]. Specifically, any assignment tolswould invalidate it.