  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.
