A Dynamic Logic for QASM Programs

We define a dynamic logic for QASM (Quantum Assembly) programming language, a language that requires the handling of quantum and probabilistic information. We provide a syntax and a model to this logic, providing a probabilistic semantics to the classical part. We exercise it with the quantum coin toss program.