Relational Denotational and Algebraic Semantics Based on UTP

Relational Hoare logic [18] extends the applicability of modular deductive verification to encompass the verification of crucial 2-run properties, such as confidentiality. Most of the current research on relational Hoare logic primarily focuses on its practical applications. However, incorporating parallel programs into the logic may further complicate the system design, which is an aspect that most research has overlooked. Therefore, this paper updates the previous system, referred to as the relational system, by incorporating parallel composition. Based on the Unifying Theories of Programming (UTP), we further explore the denotational semantics and algebraic semantics of the system with 2-runs, employing relational denotational and algebraic semantics for representation. And the study of the conditional construct and parallel composition are the crucial points. To facilitate the algebraic exploration of parallel expansion laws, we extend the system with a new concept called guarded choice, enabling the transformation of any program into a guarded choice form.