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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Relational Denotational and Algebraic Semantics Based on UTP

  • Zhiru Hou,
  • Huibiao Zhu

摘要

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.