RaML has two major modes of operation: analysis and evaluation.

1) Analysis

In analysis mode, RaML performs the automatic resource bound analysis. It outputs the bounds in form of coefficients of resource polynomials and in a simplified form where the bound is described as a polynomial in the inputs.

To analyze a program, the user has to specify a resource metric and a maximal degree of the bounds in the search space.

The standard analysis mode is the main mode. It computes a bound on resource cost of the evaluation of the last expression in the input (main expression). RaML assumes that the main expression has the form

let _ = e or e

RaML provides the option to print the resource-usage information of the functions that have been used in the main expression. RaML prints one resource-annotated function type per function call. In the web interface, RaML prints all annotated types that correspond to function calls up to depth 2 in the syntax tree.

In the module mode, RaML infers a resource bound for every top-level function in the input file. For a function that has higher-order arguments, we assume that the resource cost of calling these functions is zero. The idea is, that the resulting bound describes the cost of the higher-order function itself.

2) Evaluation

In evaluation mode, the last expression in the file (main expression) is evaluated using our resource-accounting operational big-step semantics. Again, RaML assumes that this expression is given in the form

let _ = e or e

RaML prints the result of the evaluation. It also measures and prints the resource cost as defined by the three built-in metrics heap, steps, and ticks.

Analysis modes

RaML has three analysis modes: upper bounds, lower bounds, and constant resource. The upper-bound mode derives an upper bounds on the worst-case resource behavior. The lower-bound mode derives a lower-bound on the best-case resource behavior. Finally, the constant resource mode checks if the resource consumption for a given input size is constant.


The resource usage of input programs is defined by resource metrics that assign a constant cost to each step in the big-step operational semantics. The resource bound analysis is parametric in these metrics. Metrics can be selected in the metric drop-down menu in the web interface. There are three built-in metrics:

  • Evaluation steps: number of steps in the big-step semantics
  • Heap space: number of allocated heap cells
  • Ticks: sum of evaluated tick commands

The tick metric allows the user to define a custom resource metric by annotating the code with tick commands, such as Raml.tick(1.3). This expression defines a resource usage of 1.3 resource units whenever the expression is evaluated. The argument of Raml.tick is a floating point number. A negative number expresses that resources are returned. The result type of Raml.tick is unit.


For an effective analysis we have to limit the search space for the bounds by selecting a maximal degree of the derived polynomials. The degree can be selected in the respective drop-down menu. If the selected degree is n then RaML is only able to find bounds of maximal degree n. However, RaML is still able to, for example, find a quadratic bound, even if the maximal degree is 3.

If the degree is too low then the generated linear program does not have a solution and RaML will report that it was not able to find a bound.

Known Issues

Strings and Integers

Strings and integers are currently not supported. Please use integer lists and natural numbers (see raml_runtime/

Built-in equality

Built-in equality is only supported for ground types such as integer, bool and float. Therefore is not possible to use equality in a polymorphic function. Fix: Add type annotations or make equality a function parameter.


Exceptions are currently (version 1.3) broken for the constant resource usage and lower bound analysis.