Proving asymptotic time complexity bounds with SPARK

This blog explores whether SPARK be used to prove something about the time complexities of Linear_Search and Binary_Search