  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.
