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.

翻译：确保量子程序的正确性对于量子软件质量保障至关重要。虽然针对经典程序存在多种有效的验证方法，但由于量子叠加和纠缠等执行逻辑的根本差异，这些方法无法直接应用于量子程序。这要求开发新的量子程序正确性验证方法。本文提出了一种面向量子编程语言Scaffold的行为接口规范语言（BISL），命名为ScaffML。ScaffML允许为Scaffold模块指定前置条件和后置条件，并支持在Scaffold代码中嵌入断言，从而辅助量子程序的调试与验证。本文讨论了ScaffML的设计目标与总体方法，并通过示例描述了该语言的基本特性。ScaffML为量子程序员提供了易于使用的规范语言，支持对Scaffold程序进行静态分析、运行时检测和形式化验证。最后，我们通过多个实例展示了ScaffML的工作流程与功能。