2. A Quick Introduction to Using the Resource Analysis for Hume

2.1. Basic Usage

Assume you have written a Hume program for calculating the sum of a list of floating-point numbers:


type _float = float 32;

data flist = Cons _float flist | Nil;

sum11 :: flist -> _float;
sum11 (Nil) = 0.0 ;
sum11 (Cons f fs) = f + (sum11 fs);

expression sum11;

To perform an analysis of the heap consumption of the program in sum11.hume type the following command: phamc-an -H -R sum11.hume

As a result you should see the following:


ARTHUR3 typing for HumeHeapBoxed:
 0, (flist[Cons<2>:float,#|Nil<2>]) -(0/0)-> float ,0

This is the extended type of the main expression in sum11.hume, which encodes resource information by weights attached to the constructors. This output should be read, "for a list of length n, the heap consumption of the main expression is 2*n+2".

While it is possible to do resource analysis in one go, usually, it is done in two steps, first generating an intermediate program in ARTHUR3 (.art3) or Schopenhauer, notation and then calling the resource analysis, proper:

This yields the same type as above.

We can also infer WCET bounds on the program by calling: art3 -T sum11.art3

The resource analysis, i.e. the art3 executable, has many options to tune its behaviour. Check the ART3 Manual (also available in docu/art3Manual.pdf of the distribution) for details. Both phamc-an and art3 have a --help option.

One of the most useful options is --speak (see Section Section 4.1), which delivers an explanation of the resource consumption encoded in the annotated type: art3 -H --speak sum11.art3 which yields the following output:


ARTHUR3 typing for HumeHeapBoxed:
0, (flist[Cons<2>:float,#|Nil<2>]) -(0/0)-> float ,0

Worst-case Heap-units required in relation to input:
2 + 2*X1
  where
      X1 = number of "Cons" nodes at 1. position

immediately delivering the linear bound, in terms of the input list length, discussed above.