Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT -- a type system combining fractional ownership and refinement types for imperative program verification -- with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.'s type system to support nested arrays by generalizing the notion of ownership to be able to refer to the indices of the outer arrays and prove the soundness of the extended type system. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.

翻译：Tanaka等人提出了一种类型系统，用于验证使用数组和指针算术的程序的功能正确性属性。该类型系统扩展了ConSORT——一种结合部分所有权和细化类型进行命令式程序验证的类型系统——增加了对指针算术的支持。他们的核心思想是将部分所有权扩展为可依赖数组索引的形式。然而，其形式化方法无法处理嵌套数组，而嵌套数组对于表示矩阵等实际数据结构至关重要。我们通过泛化所有权概念，使其能够引用外层数组的索引，从而扩展了Tanaka等人的类型系统以支持嵌套数组，并证明了扩展后类型系统的可靠性。我们基于所提出的类型系统实现了一个验证器，实验表明它能验证Tanaka等人方法无法处理的嵌套数组操作程序的正确性。