Abstract:
This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selingerâ¿¿s suggestion of representing quantum programs by superoperators and elucidates Dâ¿¿Hondt-Panangadenâ¿¿s theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoffâ¿¿von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal coujunctivity and termination law of quantum programs are proved, and Hoareâ¿¿s induction rule is established in the quantum setting.
