  In this paper, we study quantitative properties of quantum programs.
Properties of interest include (positive) almost-sure termination, expected
runtime or expected cost, that is, for example, the expected number of
applications of a given quantum gate, etc. After studying the completeness of
these problems in the arithmetical hierarchy over the Clifford+T fragment of
quantum mechanics, we express these problems using a variation of a quantum
pre-expectation transformer, a weakest precondition based technique that allows
to symbolically compute these quantitative properties. Under a smooth
restriction-a restriction to polynomials of bounded degree over a real closed
field-we show that the quantitative problem, which consists in finding an
upper-bound to the pre-expectation, can be decided in time double-exponential
in the size of a program, thus providing, despite its great complexity, one of
the first decidable results on the analysis and verification of quantum
programs. Finally, we sketch how the latter can be transformed into an
efficient synthesis method.
