Web Interface

How to Use the Interface


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.

Nested Patterns

RAML does currently not support nested patterns. For example,

match z with | (x::xs)::ys -> e

will not work and has to be replaced by

match z with | y::ys -> match y with | x::xs -> e

Wild cards in pattern matches

RAML currently doesn't support wild cards and variables without constructors in pattern matches. Instead of using

match z with | x::xs -> x | _ -> 0

you have to match all constructors

match z with | x::xs -> x | [] -> 0


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