PyIML Strategy

The PyIML Strategy is the formalization approach used by CodeLogician to translate Python source code into Imandra Modeling Language (IML) for formal verification and analysis.

Overview

When you point the CodeLogician server at a Python project, the PyIML strategy:

  1. Analyzes the Python source files and their dependency structure
  2. Translates Python code into equivalent IML models
  3. Manages the formalization process across the entire codebase
  4. Maintains a metamodel representing the formalized project

Key Features

Automatic Translation

  • Converts Python functions, classes, and types to IML equivalents
  • Handles common Python patterns and idioms
  • Preserves program semantics while enabling formal analysis

Dependency Management

  • Detects import relationships between modules
  • Ensures formalization order respects dependencies
  • Tracks direct and reverse dependencies

Opaque Function Handling

  • Identifies functions that cannot be directly translated to IML
  • Maintains type information while abstracting implementation
  • Allows reasoning about code even with opaque elements

Working with PyIML

The PyIML strategy automatically handles the complexity of Python-to-IML translation. You can view the generated IML models in the TUI's Model View to understand how your Python code is formalized.

Formalization States

Each Python module can be in one of several states:

  • Not Analyzed: Not yet processed by the strategy
  • Analyzing: Currently being formalized
  • Transparent: Successfully formalized with all functions implemented
  • Admitted with Opaqueness: Formalized but contains opaque functions
  • Inadmissible: Failed formalization checks

Cache Management

The strategy maintains a .cl_cache file in your project directory to:

  • Store formalization results between sessions
  • Avoid redundant analysis of unchanged files
  • Enable quick resumption of analysis

Use --clean flag when starting the server to clear the cache and start fresh.

Learn More

Previous← Server
NextTutorials →