  Quantum computing (QC) represents the future of computing systems, but the
tools for reasoning about the quantum model of computation, in which the laws
obeyed are those on the quantum mechanical scale, are still a mix of linear
algebra and Dirac notation; two subjects more suitable for physicists, rather
than computer scientists and software engineers. On this ground, we believe it
is possible to provide a more intuitive approach to thinking and writing about
quantum computing systems, in order to simplify the design of quantum
algorithms and the development of quantum software. In this paper, we move the
first step in such direction, introducing a specification language as the tool
to represent the operations of a quantum computer via axiomatic definitions, by
adopting the same symbolisms and reasoning principles used by formal methods in
software engineering. We name this approach formal quantum software engineering
(F-QSE). This work assumes familiarity with the basic principles of quantum
mechanics (QM), with the use of Zed (Z) which is a formal language of software
engineering (SE), and with the notation and techniques of first-order logic
(FOL) and functional programming (FP).
