Verifying Correct Usage of Atomic Blocks and Typestate: Technical Companion
CARNEGIE-MELLON UNIV PITTSBURGH PA INST OF SOFTWARE RESEARCH INTERNAT
Pagination or Media Count:
In this technical report, we present a static and dynamic semantics as well as a proof of soundness for a programming language presented in the paper entitled, Verifying Correct Usage of Atomic Blocks and Typestate. The proof of soundness consists of a proof of preservation, which shows that well-typed expressions evaluate to other well-typed expressions, and a proof of progress, which shows that well-typed expressions are either values or can take an evaluation step in the dynamic semantics. The notion of progress is complicated by a specific notion of a well-typed heap, which ensures that only one reference in the entire thread-pool can know the exact state of an object of share or pure permission.
- Computer Programming and Software
- Computer Systems Management and Standards