Construction and analysis of distributed systems is difficult; choreographic programming is a deadlock-freedom-by-construction approach to simplify it. In this paper, we present a new theory of choreographic programming. It supports for the first time: construction of distributed systems that require decentralised decision making (i.e., if/while-statements with multiparty conditions); analysis of distributed systems to provide not only deadlock freedom but also functional correctness (i.e., pre/postcondition reasoning). Both contributions are enabled by a single new technique, namely a predicate transformer for choreographies.
Lecture Notes in Computer Science
31st European Symposium on Programming, ESOP 2022
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Jongmans, S.-S.T.Q, & van den Bos, P. (2022). A predicate transformer for choreographies: Computing preconditions in choreographic programming. In Proceedings of the European Symposium on Programming (pp. 520–547). doi:10.1007/978-3-030-99336-8_19