Introduction

Welcome to PyIDF - a tool for analysing Python files. We will very shortly be completing this documentation site with installation instructions and background context to how to use the tool for writing Python files in the context of machine learning.

The general idea is that we constraint a Python file to model a state-transition system by insisting upon certain language features. This state transition system can then be “decomposed” using our reasoning tool imandra to provide regions which greatly enhance the efficiency of any learning that can be applied to the modelled state-transition system.

The existing documentation explains the form of the constrained file we use in order to perform the analysis by imandra. We will be completing these docs with full context version.

Installation

To install the Imandra Python module, simply run this command in your terminal:

This will install the latest version form pypi.org. The only prerequisite for the module is Python requests. No need for Imandra installation or any OCaml infrastructure.

Authentication

If you don’t have Imandra installed, we will need to authenticate you for the use of the backend of our Python module. At the first use of the module, you will be asked to follow an authentication link and given a prompt to enter the security token provided on the page.

VSCode plugin

There is an associated VSCode plugin for PyIDF which can be downloaded from within VSCode by searching for PyIDF and can be found here on the Microsoft Marketplace. This provides warnings and integration with a language server alerting the user to problems in the format of a Python file. In order for this to function correctly, there must be an executable of Python version 3.8 called python3.8 available on the PATH of the system.