Please note: These pages are work in progress!
This manual page documents the fragment of Erlang accepted by Soter.
A tipical 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.
Soter deals with a `pure' core fragment of the Erlang language.
A partial list of the unsupported features follows:
The rich module system of Erlang is not handled. Calls to external modules and module variables are not supported.
Built in functions are not supported apart from send
, self
and error
. In particular, arithmetic functions are treated as external unknown calls. Limited manipulation of natural numbers is available via the --peano
switch (see below).
Guards (when
) and type-checking functions are not supported.
Monitors, links, exception handling are currently not supported.
Impure features such as process dictionaries or registration of names is not supported.
Timeouts in receives are simply ignored.
Multi node distributed behaviour is not taken in account.
peano
OptionSince 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.
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.
?SoterOneOf
?SoterChoice
?defSoterRule
Functions defined in grammars.hrl
.
The SOTER
macro, soter:uncoverable/2
, soter:error/2
, soter:label/2
, soter:choice/2
.