Wiki

Clone wiki

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