Expanding Specification Capabilities of a Gradual Verifier with Pure Functions

TL;DR

This paper enhances a gradual verification tool by integrating pure functions, expanding its specification capabilities and simplifying observer method encoding, addressing technical challenges in axiomatisation.

Contribution

It introduces an extension to Gradual C0 with pure functions, improving expressivity and ease of encoding observer methods in gradual verification.

Findings

Extended Gradual C0 with pure functions increases specification expressivity.

Addresses axiomatisation challenges for imprecise specifications.

Improves encoding of observer methods in gradual verification.

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.