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).
翻译:量子计算(QC)代表了计算系统的未来,但计算量子模型的推理工具,即所遵循的法律是量子机械尺度的法律,仍然是线性代数和Dirac的混合体;两个主题更适合物理学家,而不是计算机科学家和软件工程师。在这一点上,我们认为可以提供一种更直观的方法来思考和写写量子计算系统,以便简化量子算法的设计和量子软件的开发。在本文件中,我们朝着这个方向迈出了第一步,采用一种规格语言作为工具,通过非轴学定义来代表量子计算机的操作,采用软件工程正规方法所使用的相同的符号和推理原则。我们用这个方法命名了正式量子软件工程(F-QSE),这项工作假定了熟悉量子力学(QM)基本原则,使用Zed(Z)是软件工程的一种正式语言,以及一阶逻辑和功能编程(FP))。