Algorithms iterating over Continuous Sparse Data are used ubiquitously in fields such as robotics, computer graphics, and scientific computing. While such algorithms are designed to solve problems involving continuous real-valued functions and operations on them such as integration, their implementations operate with discrete data, often encoded by specialised array-based representations that rely extensively on indirect indexing. This combination of continuous specification and intricate discrete implementation poses challenges for machine-assisted reasoning about Continuous Sparse Data algorithms, whose verification is largely an unexplored area to date.

We propose a novel methodology for formal specification and deductive verification of CG algorithms that operate on discrete array-encoded geometric data. For this, we adopt the recently proposed approach of using a relational Hoare-style program logic for specifying correctness of array-manipulating programs in terms of hypersafety properties (i.e., statements that relate executions of multiple programs). The key enabling idea of our work is to generalise hypersafety specifications to uncountably infinite families of programs indexed by real numbers, thereby providing an intuitive way to express statements that relate results of programs to values of continuous functions and their integrals. We developed the Logic for Continuous Data, Tensors and Vectors, dubbed LGTM∞, a new relational separation logic, which provides proof principles for real-indexed hypersafety (a.k.a. hyperreal) specifications. We demonstrate its effectiveness by mechanically verifying a set of characteristic algorithms from geo-spatial information systems and computer graphics, such as spatial count query and bilinear image interpolation.