Synopsis

-uncoverable(PROP).

?label(ID)
?label_mail(ID,EXP)

?assert_uncoverable(NUM)
?soter_error(ERRMSG)

[long textual description:] label[bound], ... .

Properties Specification

There are currently two methods to specify properties:

Through assertions
Asking soter to prove absence of error using the --prove-no-error switch

In the following section we present the syntax of assertions and the three methods to feed them into Soter:

Through assertions in the code
Writing assertions in a .prop file
Specifying a property with the --prove=PROP switch

Syntax of assertions

A single property is a list of constraints:

constr₁, constr₂, ..., constr_n

each constraint constr_i can be one of:

label >= num
label > num (equivalent to label >= num+1)
label (equivalent to label >= 1)

If a label is used in more than one constraint of the same property

l >= n₁, ..., l >= n₂, ..., l >= n_k

then these "matching" constraints all together are equivalent to the single constraint

l >= n₁+ n₂+ ... + n_k

so for example a >= 10, b, a, a, b>0 is equivalent to a >= 12, b >= 2.

A run of a program is represented by a sequence of states. A given state meets a constraint l >= n just if there are at least n processes running an instruction labelled with l at that point.

A configuration is a "bad state" wrt to a property constr~1, constr~2, ..., constr~n if it meets all the constraints.

When asked to prove such a property, Soter will try to prove that no reachable state is a bad state wrt to that property. This kind of verification problem is called coverability check hence the `uncoverable' in the names for the assertion macros.

Assertions

There are two main ways of putting assertions in the code (and they can be freely mixed).

The first method uses the ?label macro to label the relevant program points and then uses the directive

-uncoverable(PROP).

to specify a property involving those labels. As many property as needed can be specified with this method using multiple -uncoverable directives.

The second method uses inline assertions in the code via the macros explained in the dedicated section below.

Once you annotated your code with these assertions, to get them proved by Soter you need to use the --prove-assertions switch.

Inline Assertions

?label(ID)
?label_mail(ID)
?assert_uncoverable(NUM)
?soter_error(ERRMSG)

Properties file

Note: this method is available only when using the soter command-line tool, not the web interface.

A property file consists of:

Single line comments starting with % that can appear everywhere and get completely ignored by Soter
A list of properties (as described above) separated by .
Each property can be preceded by an optional description ending with :

For example:

% This is a comment
Property description:
    label1 >= 10,
    label2 > 3,
    label3, label3.

Another property: % Please document your properties!
    label > 0.

is a legal .prop file containing two properties.

When the mentioned labels are not specified in the code being analysed, the property containing them are simply ignored (and a warning is reported; warnings are only visible in verbose mode).

To ask Soter to prove the properties listed in a .prop file, use the --prop[=FILE] switch.

Single property

A single property can be specified with the switch --prove=PROP. Soter will try to prove PROP among the properties specified with the other methods.

Proving Absence Of Errors

When in "Verify Absence-of-Errors" mode, Soter will try to prove that no process will ever be in a state of error, i.e. an uncaught runtime exception. There is a limited set of such errors which are currently modelled by Soter:

sending a message to a non-pid value (e.g. "I am a string" ! {msg, hi}). Note that the register primitives are not supported so sending to an atom is always seen as "illegal" by Soter;
applying a function to the wrong number of arguments; higher-order is supported (even in messages) so this is not just a syntactic check;
applying a value that is not a function;
spawning a value that is not a function with zero arguments;
explicit calls to erlang:error.

One major omission is pattern-matching errors. Soter is currently ignoring them. The next release of Soter will feature a more precise abstract pattern-matching mechanism that will allow for pattern-matching errors to be detected avoiding too many false-alarms.

Please note that the exception handling features of Erlang, such as catch, are not currently supported by Soter. We aim to add support for them in the next release.

The Soter Macros

In order to write assertions in an Erlang module, Soter provides a set of macros defined in the file soter.hrl that can be imported by putting

-include_lib("soter.hrl").

after the -module directive and before any definition.

The header file grammars.hrl defines some commonly used non-deterministic generator of inputs (see non determinism). It depends on soter.hrl and must be imported with

-include_lib("grammars.hrl").

after every other include since it defines functions rather than macros.

Important: The inclusion of soter.hrl and grammars.hrl is automatic and implicit in the web interface; the -module and the -include_lib directives should not be used in the web interface.

Relevant Options

The full options for soter are described in soter(1). The following applies to the offline use of the tool only.

Here we list only the options which are relevant to property specifications:

-A --prove-all: attempt to prove absence of any error
-e --prove-no-error: attempt to prove absence of `error' exceptions
-a --prove-assertions: attempt to prove absence of assertion violations
-u --prove --uncoverable=PROP: tells Soter to prove the specified property.
--prop[=FILE] --prove-file: tells Soter to prove every property specified in the .prop file. If no file is specified Soter will attempt to read a .prop file with the same basename of the input Erlang module.

There are two options by which you can manually control the data abstraction parameters:

-D --val-depth=INT: specifies a depth for the data abstraction
-M --msg-depth=INT: specifies a depth for the message abstraction

SOTER 0.1 | Specifications

Emanuele D'Osualdo

Jonathan Kochems

Luke Ong