Predicate transformers as power operations |
| |
| Authors: | I Rewitzky C Brink |
| |
| Affiliation: | (1) Laboratory for Formal Aspects and Complexity in Computer Science, Department of Mathematics, University of Cape Town, 7700 Rondebosch, South Africa |
| |
| Abstract: | In predicate transformer semantics, a program is represented as a mapping from predicates to predicates. In relational semantics, a program is represented as an (input-output) binary relation over some state space. We show how each of these approaches can be obtained from the other by using thepower construction. |
| |
| Keywords: | Binary relation Boolean algebra Predicate transformer semantics Relational semantics Weakest precondition |
| 本文献已被 SpringerLink 等数据库收录！ |
