Imandra python: formal verification and reasoning about python programs
imandra is a Python client for the Imandra - a cloud-native automated reasoning engine built on the latest advances in formal verification and symbolic reasoning.
The client idiomatically exposes Imandra Iterative Decomposition Framework (IDF) functionality to decompose state-transition algorithms. The client accepts a sting containig the Python code to decompose - see the documentation to learn how to write an accepted model code:
code = """ class State: def __init__(self): self.x : int = 0 def receive_Update(self, v : int): self.x : int = v scenario = [ 'Update' , 'Update' ] """
You can launch an IDF decomposition job in the cloud with
imandra.idf.decompose, passing it the code string:
from imandra import idf decomposition = idf.decompose(code)
decomposition object as a handle, you can check the status of the job which can be in
When the decomposition job is finised, you can obtain the generated Python code for the regions:
# Create a separate Python function per region predicate print(decomposition.dumps(kind='flat')) # Create a single optimized function that returns a region number print(decomposition.dumps(kind='tree'))
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
|Filename, size & hash||File type||Python version||Upload date|
|imandra-0.1.5-py3-none-any.whl (9.4 kB) View hashes||Wheel||py3|
|imandra-0.1.5.tar.gz (4.3 kB) View hashes||Source||None|