CONTENTS

This manual page documents the fragment of Erlang accepted by Soter.

Recent versions of the Erlang compiler introduced some breaking changes to Core Erlang. The latest version of Erlang known to be compatible with Soter is version 20. See here for more details.

Input Erlang Programs

A typical Erlang module that can be analysed by Soter looks like the following:

-module(example).
-compile(export_all).

-include_lib("soter.hrl").

-soter_config(peano).

-uncoverable("wrong_incipit > 0").

main() ->
    N = any_nat(),
    P = spawn(fun()-> f(N) end),
    P ! {hi, self()} ,
    receive
        X -> X
    end.

any_nat() -> ?SoterChoice(
        fun()-> 0 end,
        fun()-> any_nat()+1 end
    ).

f(N) ->
    receive
        {hi, P} ->
            P ! {hey, N}
            start_protocol(N, P);
        bla ->
            ?label(wrong_incipit),
            complain(N)
    end.

...

The soter.hrl library is included and makes the Soter macros such as ?SoterChoice or ?label, available.

The directive -soter_config sets some Soter options.

The -uncoverable directive is one way of specifying a property to be proved by Soter.

There is a main/0 function which serves as entry point for the program.

The definition of any_nat makes use of one of the Soter macros which introduce a non-deterministic choice; in this example any_nat would be able to non-deterministically generate every positive integer.

The other definitions are standard Erlang definitions which must meet some constraints outlined in the Limitations section.

All the modules accepted by Soter can be executed with the Erlang interpreter without modification and are valid Erlang programs.

Limitations

Soter deals with a `pure' core fragment of the Erlang language.

A partial list of the unsupported features follows:

Recent versions of the Erlang compiler introduced some breaking changes to Core Erlang. The latest version of Erlang known to be (mostly) compatible with Soter is version 20.

If you encounter errors, a common source of incompatibility is compiler annotations around generated variables, a situation that arises from using the catch-all pattern _. Try and use a throw-away variable name like _1 instead. For example, a pattern like:

case {a,b} of
    _ -> ok
end.

might need to be rewritten as

case {a,b} of
    {_1, _2} -> ok
end.

The peano Option

Since arithmetic operations are not currently supported, all the data-types need to be constructed as trees using the tuple and list constructors plus atoms. For example, integers can be encoded using the atom zero as a representation for 0 and {s, N} as a representation for the successor of a number N. Since writing numbers and operations with this notation can be cumbersome, Soter offers the --peano option which treats integer literals as syntactic sugar for numbers encoded as illustrated above. Addition/subtraction to a constant is translated in the corresponding operation on peano numbers. These are the only supported arithmetic operations when the peano option is selected.

From the code the peano option can be activated by inserting the directive

-soter_config(peano).

Note: if the peano option is switched off, any call to + or - will be translated to a "dead-end" node representing a call to an unknown function.

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

Non determinism

?SoterOneOf
?SoterChoice
?defSoterRule

Configuration

Directives:

-soter_config(OPT).

Input generators

Functions defined in grammars.hrl.

Implementation of the macros

The SOTER macro, soter:uncoverable/2, soter:error/2, soter:label/2, soter:choice/2.