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*.

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.

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

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.

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*

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.