Formal software verification techniques are widely used to specify and prove the functional correctness of programs. However, nonfunctional properties such as time complexity are usually carried out with pen and paper. Inefficient code in terms of time complexity may cause massive performance problems in large-scale complex systems. We present a proof of concept for using the Dafny verification tool to specify and verify the worst-case time complexity of binary search. This approach can also be used for academic purposes as a new way to teach algorithms and complexity.

翻译：正式的软件核查技术被广泛用来说明和证明程序在功能上的正确性,但是,时间复杂性等不起作用的特性通常是用笔和纸进行的,时间复杂性方面的编码效率低下可能会在大型复杂系统中造成大规模的性能问题。我们为使用Dafny核查工具来确定和核实二进制搜索的最坏情况的复杂性提供了一个概念证明。这个方法也可以用于学术目的,作为教授算法和复杂性的新方法。