ScaffML: A Quantum Behavioral Interface Specification Language for Scaffold
Tiancheng Jin, Jianjun Zhao

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Computing Algorithms and Architecture · Logic, programming, and type systems · Cloud Computing and Resource Management
