Prototype Introduction

Environment

The Prototype is written in Python 3 with an output of Matlab file (.m). To conduct the Invariant, Matlab version of YALMIP and SeDuMi toolboxes are needed. For YALMIP toolbox, one can find the latest version in https://yalmip.github.io/. For semidefinite programming, we use SeDuMi solver, of which the homepage is http://sedumi.ie.lehigh.edu/.

Synthesize quantitative loop invariant

To synthesize an invariant for simple loops in probabilistic programs, one need to create a python file to input details about the program. The format can be seen from our provided example with tool.py and main.py needed to be imported. After inputing all the details, one needs to create a Matlab_file class defined in tool.py, run the create_file function, and name the output file. Then by executing the output file, one can get an executable Matlab file in the same path as your python file.

variables = []  # the variables should be input as a list, with each variable as a string, and comma as split symbol
pre_exp  = '' # a string for pre_exp
post_exp = '' # a string for post_exp
while_sentence = '' # in the form of 'sentence1[p]sentence2', cannot deal with several sentences yet
while_valuation = [] # a list for the valuation sentence in while loop, each valuation should be written as a string
while_condition = '' # a string denoting while condition, use 'and' or 'or' in the string to denote logical relationship
addition_condition = [] # denoting constraint refinements, each constraint is a string
initial_value = [] # denoting the initial valuation for the loop, each valuatio is a string

Then the class matlab_File is constructed and the function create_file can create the related matlab file.

An interface is also provided to make user input more convenient. The user still needs to input the items mentioned in the table above, but not in the formation of programming language. The following picture shows an example.

"maximum degree of template" can be remained empty and the programme will use a default value. Since we cannot assume a default installation path for Matlab in user's computer, the interface also generates a matlab file that needs the user to execute manually.

Prototype

Examples

Examples for nested loop programs are also provided here, but not yet supported by our prototype, so only matlab files are presented.