Presburger-Definable Parameterized Typestates

TL;DR

This paper introduces parameterized typestates (p-typestates) that extend traditional typestates with logical properties, enabling the specification and verification of non-finite-state program properties using dependent types and Presburger-definable transition systems.

Contribution

It proposes a dependent type system for p-typestates and a method to automatically compute loop invariants via loop acceleration techniques.

Findings

Able to specify non-finite-state properties beyond traditional typestates

Developed a type-checking approach with automatic invariant calculation

Enhanced program verification with logical properties in typestates

Abstract

Typestates are good at capturing dynamic states of a program as compared to normal types that can capture static structural properties of data and program. Although useful, typestates are suitable only for specifying and verifying program properties defined using finite-state abstractions. Many useful dynamic properties of programs are not finite-state definable. To address these issues, we introduce parameterized typestates (p-typestates). p-typestates associate a logical property with each state of regular typestate, thereby allowing specification of properties beyond finite-state abstractions. We present a dependent type system to express and verify p-typestate properties and a typestate-oriented core programming language incorporating these dependent types. Automatic inductive type-checking of p-typestate properties usually requires a programmer to provide loop invariants as annotations. Here we propose a way to calculate loop invariants automatically, using loop acceleration techniques for Presburger definable transition systems. \keywords{Programming Languages, Typestates, Dependent Types, Non-Regular Program Properties, Verification, Loop Invariants}