This technical report contains detailed definitions, auxiliary lemmas, main theorems, and proofs related to the paper A Predicate Transformer for Choreographies, published in the proceedings of ESOP 2022. The aim of this document is to provide a comprehensive reference guide for the theory presented in the paper. In contrast to the paper, we do not split the presentation into a base calculus, an extension with blocking if/while-statements, and an extension with non-blocking if/while statements. Instead, we present the whole calculus of global programs, including all extensions, at once.
|Place of Publication||Heerlen|
|Publisher||Open Universiteit Nederland|
|Number of pages||132|
|Publication status||Published - 2022|
|Series||OUNL-CS (Technical Reports)|