ScaffML: A Quantum Behavioral Interface Specification Language for Scaffold

TL;DR

ScaffML is a new behavioral interface specification language designed for the quantum programming language Scaffold, enabling formal verification, static analysis, and debugging of quantum programs to improve software correctness.

Contribution

It introduces ScaffML, the first BISL for Scaffold, supporting pre- and post-conditions, assertions, and verification methods tailored for quantum programming.

Findings

Supports static analysis and run-time checking

Facilitates debugging and verification of quantum programs

Provides an easy-to-use specification language for quantum developers

Abstract

Ensuring the correctness of quantum programs is crucial for quantum software quality assurance. Although various effective verification methods exist for classical programs, they cannot be applied to quantum programs due to the fundamental differences in their execution logic, such as quantum superposition and entanglement. This calls for new methods to verify the correctness of quantum programs. In this paper, we present a behavioral interface specification language (BISL) called ScaffML for the quantum programming language Scaffold. ScaffML allows the specification of pre- and post-conditions for Scaffold modules and enables the mixing of assertions with Scaffold code, thereby facilitating debugging and verification of quantum programs. This paper discusses the goals and overall approach of ScaffML and describes the basic features of the language through examples. ScaffML provides an easy-to-use specification language for quantum programmers, supporting static analysis, run-time checking, and formal verification of Scaffold programs. Finally, we present several instances to illustrate the workflow and functionalities of ScaffML.