Imandra CodeLogician: VS Code

Use Imandra CodeLogician to formalize and analyze Python code.

Features

• Translate Python files into formal (precise) mathematical models expressed in Imandra Modelling Language (IML).
• Apply Automated Reasoning techniques to the formal model, including:
  • Reverse-engineering inputs to functions.
  • Decomposing complex functions into (finite) symbolic regions of invariant behaviour.
  • Identify edge cases where functions do not behave as expected.
• Integrate with the Imandra X Extension to explore the generated models.

Requirements

• The Imandra X Extension (and its dependencies) is recommended to fully utilise formalized code.
• The Python Extension is recommended to provide symbol analysis (identifying functions) on Python files.

Extension Settings

You can configure CodeLogician with the following settings:

• imandra.codeLogician.apiKey: Set your Imandra Universe API key here. By default, this is inferred from the IMANDRA_API_KEY environment variable and then from the contents of ~/.config/imandra/api_key (or ~/.config/imandrax/api_key).
• imandra.codeLogician.formalization.refactorFirst: Controls whether to refactor Python code before formalizing. Refactoring code first can improve the formalization of challenging Python code, but risks introducing behavioural changes. Options are:
  • always: Always refactor Python code before formalizing.
  • never: Formalize Python code directly without refactoring.
  • ask (default): Ask whether to refactor each time.