# llStar / Specification

The specification of a function is simply a pair of formulas describing the precondition expected by the function, and the postcondition that results from executing the function starting from the precondition.

## Syntax

A specification for the function `fun` is written:

```fun: {pre}{post}
```

where `pre` and `post` are formulas that may mention function parameters and a return value. Existential variables appearing in these formulas are quantified across the whole triple.

The precondition `pre` describes the initial state that is supposed to exist every time the function `fun` is invoked, while the postcondition `post` describes the state after the execution of the function.

### Parameters

The specification of a function may refer to the arguments of the function as `@parameter0:`, `@parameter1:`, etc.

### Return values

If the function returns a value, it can be referred to in the specification using the special variable `\$ret_v1`.

## Examples

The specs of some functions are defined by default by llStar, for instance for `malloc` and `free` (found in specs/stdlib.spec ):

```malloc:
{}
{(\$ret_v1 != NULL()
* malloced(\$ret_v1,@parameter0:)
* pointer(\$ret_v1,array_type(@parameter0:,integer_type("8")),_v))
|| \$ret_v1 = NULL()}

free:
{malloced(@parameter0:,?s) * pointer(@parameter0:,array_type(?s,integer_type("8")),_v)}
{}
```

In the case of `malloc`, nothing is required in the precondition (`{}`), and, after the call has completed, the state either is a non-null pointer to an array of byte of the size corresponding to the argument of `malloc`, together (`*`) with a token `malloced(\$ret_v1,@parameter0:)` recording the fact that the pointer was allocated by `malloc` (see Formulas). The call might also fail and return an empty heap and a value equal to the null pointer. In either case, the address of the pointer is returned by the function, as indicated by the special variable `\$ret_v1`.

Similarly, the spec for `free` takes a malloced pointer and removes it. Notice that the size of the array of bytes pointed to by the pointer and the size recorded by the `malloced` predicate have to match.

Updated