Skip to main content

A runtime verification framework

Project description

# pythonrv

pythonrv is a runtime verification framework for python. It is the
implementation of a master thesis currently being written. Please see
[]( for more

[![Build Status](](

## Installing

pythonrv is available as a [pip package](,
with and everything. Use
[pip]( to install it like

pip install pythonrv

pythonrv has been tested with Python 2.7. It does not yet work with Python 3.

## Coding

Clone the repository:

git clone
cd pythonrv

Initialize the environment (preferrably through
[virtualenv](, and possibly

pip install -r requirements.txt

Run the tests:


## Runtime Verification

Runtime verification is the idea of verifying the correctness of a program
during its execution. Verification is done by checking if the program conforms
to its specifications.

There are several approaches to runtime verification, where pythonrv is one. It
is based on the idea that the specifications should be written in the target
programming language, in a similar manner to unit tests, and therefore make
them both more expressive and easier to learn.

The specifications written in pythonrv get "baked" into the target's source
code, so that whenever a function is called the specifications are executed as

## Examples

Here are some simple examples showing the pythonrv API. For more realistic
examples, see the
[examples]( folder.
The [unit
tests]( might
also be useful to see what works.

First, lets say we have a function which correctness we want to verify:

~~~ python
def factorial(n):
res = 1
for i in range(2, n)
res *= i
return res

We can now write specifications for it, preferably in another file:

~~~ python
from pythonrv import rv
import factorial

def input_only_spec(event):
assert event.fn.fact.inputs[0] >= 0

def simple_specification(event):
assert event.fn.fact.result >= event.fn.fact.inputs[0]

@rv.spec(when=rv.POST, history_size=rv.INFINITE_HISTORY_SIZE)
def simple_specification(event):
in_out = (event.fn.fact.inputs[0], event.fn.fact.result)
old_in_out = [(x.inputs[0], x.result) for x in event.fn.fact.history]

for a in old_in_out:
if in_out[0] > old_in_out[0]:
assert in_out[1] >= old_in_out[1]

The first specification checks that all inputs are greater-than-or-equal-to
The second specification checks that all outputs are at least as big as the
inputs. The third specification verifies the input/output against the
historical data for the function; given a larger input, the output must be
larger-or-equal than before. Note that the last two specs are executed after
the factorial has been called. This gives them access to return values and
output arguments.

A specification is sent an event with information of the called function, its
history, and the history of all functions monitored by the specification.

~~~ python
from pythonrv import rv
import mymodule

@rv.spec(when=rv.POST, history_size=20)
def more_specifications(event):
# here are all functions monitored
# the currently called function can be accessed like this
# which, if was called, is the same as

# we can also check if a function was called

# the inputs, outputs and result can be accessed like this # a copy of the input argument tuple # a copy of the input key-word argument dict

# we can gain access to the previous event, and the previous function call

# if two calls to occurr consecutively
assert ==
# but they needn't be if more than one function is monitored by a spec

# we can gain access to the "entire" history
for old_event in event.history:
# and
for old_foo_call in
# this is obviously a big drain on the memory, so by default only two events
# are stored in the history (this and the previous). this can be changed,
# like we do here with @rv.spec(history_size=20)

# we can also say that the next time some monitored function is called,
# something should happen

# or for just a specific monitored function

# we can also specify which monitored function should be the next to be
# called:

# sometimes a specification can "finish" - it need not be verified again
event.success("optional message telling that everything was ok")
# or
event.failure("we've failed, and there's no point continuing this verification")

def call_next_time(event):
# here we gain access to all the same data as in the spec

## When to Execute the Specification

The specification is executed before the call is passed on to the active
monitoree. This can be customized:

~~~ python
def spec_after(event):

# this is the default, it is not needed to explicitly specify PRE
def spec_before(event):

## Dealing with Errors

Specifications signal verifications errors by raising the `AssertionError`
exception (which the `assert` statement does). When this happens, pythonrv, by
default, lets this error propagate, and, if uncaught, the program stops.

If this is not the desired behaviour, it can be changed. For a logging error
handler, do

~~~ python
from pythonrv import rv

and then configure logging the normal way, through the [python logging

Specifications can be marked with an error level:

~~~ python
def spec(event):

The available error levels are DEBUG, INFO, WARNING, ERROR and CRITICAL (just
as in the logging module).

For more on error handling, see the [source
code](, and the

## Technical Issues

### Importing
It is recommended that you import your rv specifications among the first things
you do in your program. The reasons will be detailed below.

When writing specs, this is the **wrong** way:

~~~ python
# this doesn't work
from mymodule import myfunc
def spec(event):

This is the correct way:

~~~ python
# this works
import mymodule
def spec(event):

The first example creates a reference to myfunc and inserts it into the
current module (the module defining the specification). Monitoring a function
means adding a wrapper around it, and in this case we only add a wrapper for
the myfunc reference in the current module. We do not modify mymodule, which
all other code will use. The second example fixes this.

The above reason also explains why the specifications should be
imported/defined at the very beginning of the execution: Other modules might
use the from x import y style, and if they do so before the rv specifications
have had a chance to monitor/instrument the functions, they will get
unmonitored/uninstrumented references to them.

### Copying arguments

When intercepting function calls, pythonrv copies the arguments to make sure
that the history it stores doesn't get altered afterwards and/or from the
outside. This also makes it so that the input arguments really are input
arguments, and not modified by the function itself.

This might sometimes be deemed unnecessary, or needlessly expensive. It might
sometimes not even work, for instance when
[`cStringIO`]( is involved. This
is the case for [Django]( requests in v1.4.x
(but not on master).

Copying can be turned off for all specifications:

~~~ python
from pythonrv import rv

Or for a specific specification:

~~~ python
from pythonrv import rv
def spec(event):

Note: Disabling argument copying for one specification actually disables
argument copying for all monitored functions for that specification. Other
specifications that monitor the same functions won't get argument copying
either. This is "a feature".

## License

pythonrv is released under the [MIT

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

pythonrv-0.1.3.tar.gz (23.6 kB view hashes)

Uploaded source

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Huawei Huawei PSF Sponsor Microsoft Microsoft PSF Sponsor NVIDIA NVIDIA PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page