Open DavePearce opened 3 years ago
Some observations about array types:
int[]
int[8]
int[n]
n
int[?]
Based on this model, we can extend to references as follows:
&int
&int:1
&int:n
&int:?
An interesting question here is how you create an instance of e.g. &int:2. Presumably, something like the following would be necessary:
&int:2
&int:1 p = new 123 (&int:2 q, &int:2 r) = (p,p)
A similar question is how you would destroy such a reference.
Some observations about array types:
int[]
is a dynamically sized array with a known length. Accesses can be checked.int[8]
is a fixed-size array. Again, accesses can be checked.int[n]
is a dynamically sized array with a known length determined by some variablen
currently in scope. Again, accesses can be checked.int[?]
is a dynamically sized array with an unknown length. Accesses cannot be checked.Based on this model, we can extend to references as follows:
&int
is a reference with an dynamically sized but known number of referents. Deletion can be checked.&int:1
is a reference with a statically sized known of references. Deletion can be checked.&int:n
is a reference with a dynamically sized number of referents determined by some variablen
currently in scope. Again, deletion can be checked.&int:?
is a reference with an unknown number of referents. Deletion cannot be checked (though it could be disallowed).An interesting question here is how you create an instance of e.g.
&int:2
. Presumably, something like the following would be necessary:A similar question is how you would destroy such a reference.