2018/02/23 by Eduard Kamburjan, Kamburjan, Eduard, Tzu‐Chun Chen +2
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.PL
paper · pdf · doi:10.48550/arxiv.1802.08492
Technical report for the paper "Stateful Behavioral Types for Active Objects" at iFM'18
openalex publication_date 2018/02/23 · arxiv created 2018/06/25 · arxiv updated 2018/06/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
It is notoriously hard to correctly implement a multiparty protocol which involves asynchronous/concurrent interactions and the constraints on states of multiple participants. To assist developers in implementing such protocols, we propose a novel specification language to specify interactions within multiple object-oriented actors and the side-effects on heap memory of those actors; a behavioral-type-based analysis is presented for type checking. Our specification language formalizes a protocol as a global type, which describes the procedure of asynchronous method calls, the usage of futures, and the heap side-effects with a first-order logic. To characterize runs of instances of types, we give a model-theoretic semantics for types and translate them into logical constraints over traces. We prove protocol adherence: If a program is well-typed w.r.t. a protocol, then every trace of the program adheres to the protocol, i.e., every trace is a model for the formula of its type.