Expanding Specification Capabilities of a Gradual Verifier with Pure Functions
Doruk Alp Mutlu
TL;DR
This paper addresses the limited expressivity of Gradual C0's specification language within gradual verification. It proposes extending Gradual C0 with pure, side-effect-free functions to improve specification clarity and ease observer-method encoding, supported by revised axiomatisation and evaluation rules in the Gradual Viper engine. The approach tackles imprecision by extending function snapshots with missing permissions and carefully managing runtime checks, while outlining rejection criteria for imprecise recursive predicates. A factorial example demonstrates the practical benefit of using pure functions to verify iterative methods, and the work highlights future steps toward implementation and formal soundness proofs.
Abstract
Gradual verification soundly combines static checking and dynamic checking to provide an incremental approach for software verification. With gradual verification, programs can be partially specified first, and then the full specification of a program can be achieved in incremental steps. The first and only practicable gradual verifier based on symbolic execution, Gradual C0, supports recursive heap data structures. Despite recent efforts to improve the expressivity of Gradual C0's specification language, Gradual C0's specification language is still limited in its capabilities for complex expressions. This work explores an extension to Gradual C0's design with a common construct supported by many static verification tools, pure functions, which both extend the specification capabilities of Gradual C0 and increase the ease of encoding observer methods in Gradual C0. Our approach addresses the technical challenges related to the axiomatisation of pure functions with imprecise specifications.