Formal Quantum Software Engineering: Introducing the Formal Methods of Software Engineering to Quantum Computing

TL;DR

This paper introduces a formal specification language for quantum computing systems, applying software engineering principles to simplify quantum algorithm design and development.

Contribution

It proposes the first formal methods-based approach, called formal quantum software engineering (F-QSE), for representing quantum operations axiomatically using familiar software engineering symbols.

Findings

Developed a specification language for quantum systems

Applied formal methods to quantum computing modeling

Facilitated intuitive reasoning about quantum algorithms

Abstract

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).