Accession Number:

ADA488523

Title:

Verifying Correct Usage of Atomic Blocks and Typestate: Technical Companion

Descriptive Note:

Technical rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA INST OF SOFTWARE RESEARCH INTERNAT

Personal Author(s):

Report Date:

2008-08-01

Pagination or Media Count:

44.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE