Verifying Time Complexity of Binary Search using Dafny

TL;DR

This paper demonstrates how the Dafny verification tool can be used to formally specify and verify the worst-case time complexity of binary search, bridging the gap between functional correctness and performance guarantees.

Contribution

It introduces a novel method for verifying nonfunctional properties like time complexity using formal verification tools, specifically Dafny, for educational and practical purposes.

Findings

Successfully verified worst-case time complexity of binary search

Proposed a new approach for formal complexity verification

Potential for improved teaching of algorithms and complexity

Abstract

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.