Analyzing Sorting Algorithms in Resource Aware ML

Abstract

Software development sometimes requires to statically predict the quantity of resources—such as memory and time—that is needed to execute a program. The difficulties of manual resource analysis led to extensive research on automatic methods for quantitative resource analysis. Recently we developed an automatic amortized analysis to compute polynomial resource bounds for first-order functional programs at compile time. Its basis is a type system that augments types with resource annotations. The analysis system is integrated in the programming language Resource Aware ML. Our experiments with a prototype implementation show that the analysis efficiently computes precise time and heap-space bounds for many example programs. In this paper I demonstrate how a user can employ Resource Aware ML to analyze the worst-case time behavior of the sorting algorithms quick sort, insertion sort and merge sort. To illustrate pros and cons, I compare our automatic analysis to a manual analysis of the algorithms in a standard textbook. The paper is divided into three sections. Section 1 motivates the research on static resource analysis. Section 2 briefly introduces Resource Aware ML. Finally, Section 3 contains the actual case study on sorting algorithms.