  We investigate the formal semantics of a simple imperative language that has
both classical and quantum constructs. More specifically, we provide an
operational semantics, a denotational semantics and two Hoare-style proof
systems: an abstract one and a concrete one. The two proof systems are
satisfaction-based, as inspired by the program logics of Barthe et al for
probabilistic programs. The abstract proof system turns out to be sound and
relatively complete, while the concrete one is sound only.
