python-to-dafny-translator

Python to Dafny Translator

Overview

Transform Python programs into equivalent Dafny code that preserves the original semantics while adding formal specifications and leveraging Dafny's verification capabilities.

Translation Workflow

Step 1: Analyze Python Code

Understand the Python program structure and semantics:

1. Identify program components:

   • Functions and their signatures
   • Classes and methods
   • Data structures (lists, dicts, sets)
   • Control flow (loops, conditionals)
   • Variable types (infer from usage)

2. Understand semantics:

   • What does the program compute?
   • What are the inputs and outputs?
   • What are the preconditions and postconditions?
   • Are there invariants or constraints?

3. Note translation challenges:

   • Dynamic typing
   • Mutable data structures
   • Exception handling
   • Python-specific features (list comprehensions, generators)

Step 2: Design Dafny Structure

Plan the Dafny equivalent:

1. Choose appropriate types:

   • int for integers (arbitrary precision)
   • nat for non-negative integers
   • bool for booleans
   • string for strings
   • real for floating-point (when needed)
   • seq<T> for lists
   • set<T> for sets
   • map<K, V> for dictionaries
   • array<T> for mutable arrays

2. Determine function vs method:

   • Function: Pure computation, no side effects, used in specifications
   • Method: Can have side effects, modify state, perform I/O

3. Plan specifications:

   • Preconditions (requires)
   • Postconditions (ensures)
   • Loop invariants
   • Frame conditions (modifies, reads)

Step 3: Translate Code

Follow these translation principles:

Functions

Pattern: Pure function

# Python
def add(a, b):
    return a + b

// Dafny
function add(a: int, b: int): int
{
    a + b
}

Pattern: Function with specifications

# Python
def max_value(a, b):
    """Returns the maximum of a and b"""
    return a if a > b else b