2017/12/23 by Ashish Mishra, Mishra, Ashish, Deepak D’Souza +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1712.08753
openalex publication_date 2017/12/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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. \keywordsProgramming Languages, Typestates, Dependent Types, Non-Regular Program Properties, Verification, Loop Invariants