IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.
Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?
Some algorithms such as binary search give an incorrect view of the overall cost. The search has a prerequisite of sorting. So, the assumption is, the data is sorted once, and searched several times, making the sorting cost insignificant.
What if the data is used for only a single lookup? For this case, actually a sequential search would have lower cost compared to sorting and binary search. Infact, sequential search may beat sorting and binary search for upto about 100 lookups. So I think it is important to consider overall cost.
But how the data got sorted is irrelevant to the speed of the algorithm: for example, you could use binary search as part of an algorithm to find the insertion point of a new element in an always sorted data structure, meaning that sorting the data is never necessary.
IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.
Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?
Some algorithms such as binary search give an incorrect view of the overall cost. The search has a prerequisite of sorting. So, the assumption is, the data is sorted once, and searched several times, making the sorting cost insignificant.
What if the data is used for only a single lookup? For this case, actually a sequential search would have lower cost compared to sorting and binary search. Infact, sequential search may beat sorting and binary search for upto about 100 lookups. So I think it is important to consider overall cost.
But how the data got sorted is irrelevant to the speed of the algorithm: for example, you could use binary search as part of an algorithm to find the insertion point of a new element in an always sorted data structure, meaning that sorting the data is never necessary.