Many program optimizations and analyses, such as array-bounds
checking, termination analysis, depend on knowing the size of a function's
input and output. However, size information can be difficult to compute.
Firstly, accurate size computation requires detecting a size relation
between different inputs of a function. Secondly, size information may
also be contained inside a collection (data structure with multiple
elements).
[1] introduces some techniques for deriving universal and existential size
properties over collections of elements of recursive data structures. It
is shown how a mixed constraint system could support the enhanced size
type, and examples where collection analysis is useful are being
highlighted. In order to support such mixed constraints, Isabelle theorem
prover has been used for implementing the system. Isabelle provides useful
proof procedures for various first-order and higher-order logics handling
both size and collection analyses.