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:
2. Functions and their signatures
3. Classes and methods
4. Data structures (lists, dicts, sets)
5. Control flow (loops, conditionals)
6. Variable types (infer from usage)

1. Understand semantics:
2. What does the program compute?
3. What are the inputs and outputs?
4. What are the preconditions and postconditions?
5. Are there invariants or constraints?

1. Note translation challenges:
2. Dynamic typing
3. Mutable data structures
4. Exception handling
5. Python-specific features (list comprehensions, generators)

Step 2: Design Dafny Structure

Plan the Dafny equivalent:

1. Choose appropriate types:
2. int for integers (arbitrary precision)
3. nat for non-negative integers
4. bool for booleans
5. string for strings
6. real for floating-point (when needed)
7. seq<T> for lists
8. set<T> for sets
9. map<K, V> for dictionaries
10. array<T> for mutable arrays

1. Determine function vs method:
2. Function: Pure computation, no side effects, used in specifications
3. Method: Can have side effects, modify state, perform I/O

1. Plan specifications:
2. Preconditions (requires)
3. Postconditions (ensures)
4. Loop invariants
5. 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

// Dafny
function max(a: int, b: int): int
    ensures max(a, b) >= a && max(a, b) >= b
    ensures max(a, b) == a || max(a, b) == b
{
    if a > b then a else b
}

Methods

Pattern: Method with side effects

# Python
def increment_counter(counter):
    counter[0] += 1

// Dafny
method incrementCounter(counter: array<int>)
    requires counter.Length > 0
    modifies counter
    ensures counter[0] == old(counter[0]) + 1
{
    counter[0] := counter[0] + 1;
}

Control Flow

Pattern: If-else

# Python
def abs_value(x):
    if x < 0:
        return -x
    else:
        return x

// Dafny
function abs(x: int): int
    ensures abs(x) >= 0
{
    if x < 0 then -x else x
}

Pattern: For loop → While loop with invariants

# Python
def sum_array(arr):
    total = 0
    for i in range(len(arr)):
        total += arr[i]
    return total

// Dafny
method sumArray(arr: array<int>) returns (total: int)
{
    total := 0;
    var i := 0;
    while i < arr.Length
        invariant 0 <= i <= arr.Length
        invariant total == sum(arr[..i])
    {
        total := total + arr[i];
        i := i + 1;
    }
}

function sum(s: seq<int>): int
{
    if |s| == 0 then 0 else s[0] + sum(s[1..])
}

Collections

Pattern: Lists → Sequences

# Python
lst = [1, 2, 3, 4, 5]
first = lst[0]
length = len(lst)

// Dafny
var lst: seq<int> := [1, 2, 3, 4, 5];
var first: int := lst[0];
var length: int := |lst|;

Pattern: Dictionaries → Maps

# Python
d = {"a": 1, "b": 2}
value = d["a"]

// Dafny
var d: map<string, int> := map["a" := 1, "b" := 2];
var value: int := d["a"];

Classes

Pattern: Simple class

# Python
class Point:
    def __init__(self, x, y):
        self.x = x
        self.y = y

    def move(self, dx, dy):
        self.x += dx
        self.y += dy

// Dafny
class Point {
    var x: int
    var y: int

    constructor(x: int, y: int)
        ensures this.x == x && this.y == y
    {
        this.x := x;
        this.y := y;
    }

    method move(dx: int, dy: int)
        modifies this
        ensures x == old(x) + dx
        ensures y == old(y) + dy
    {
        x := x + dx;
        y := y + dy;
    }
}

Step 4: Add Specifications

Enhance the Dafny code with formal specifications:

1. Preconditions (requires):
2. What must be true before the function/method executes?
3. Example: requires n >= 0 for factorial

1. Postconditions (ensures):
2. What is guaranteed after execution?
3. Example: ensures result >= 0 for absolute value

1. Loop invariants:
2. What is true at the start of each iteration?
3. Example: invariant 0 <= i <= n for loop counter

1. Frame conditions:
2. modifies: What can be modified?
3. reads: What can be read?

Step 5: Verify and Test

Ensure the translated code is correct:

1. Run Dafny verifier:

``bash dafny verify program.dfy ``

1. Fix verification errors:
2. Add missing invariants
3. Strengthen postconditions
4. Add helper lemmas if needed

1. Test execution:

``bash dafny run program.dfy ``

1. Compare outputs:
2. Run original Python program
3. Run translated Dafny program
4. Verify outputs match

Step 6: Refine and Optimize

Improve the translated code:

1. Simplify specifications:
2. Remove redundant conditions
3. Use helper functions for complex specs

1. Add documentation:

``dafny // Computes the factorial of n function factorial(n: nat): nat ``

1. Optimize for verification:
2. Break complex functions into smaller pieces
3. Add intermediate assertions
4. Use lemmas for complex proofs

Common Translation Patterns

For detailed patterns, see [translation_patterns.md](references/translation_patterns.md).

Quick Reference

| Python | Dafny | |--------|-------| | x = 10 | var x: int := 10; | | def f(x): | function f(x: int): int or method f(x: int) | | return x | x (function) or return x; (method) | | if x > 0: | if x > 0 then or if x > 0 { | | for i in range(n): | while i < n with invariants | | [1, 2, 3] | [1, 2, 3] (seq) | | {1, 2, 3} | {1, 2, 3} (set) | | {"a": 1} | map["a" := 1] | | len(lst) | \|lst\| | | lst[i] | lst[i] | | class C: | class C { | | None | Use Option<T> datatype |

Examples

Example 1: Simple Function

Python Input:

def factorial(n):
    if n <= 1:
        return 1
    return n * factorial(n - 1)

Dafny Output:

function factorial(n: nat): nat
    ensures factorial(n) >= 1
{
    if n <= 1 then 1
    else n * factorial(n - 1)
}

Example 2: Array Processing

Python Input:

def find_max(arr):
    if len(arr) == 0:
        return None
    max_val = arr[0]
    for i in range(1, len(arr)):
        if arr[i] > max_val:
            max_val = arr[i]
    return max_val

Dafny Output:

method findMax(arr: array<int>) returns (maxVal: int)
    requires arr.Length > 0
    ensures forall k :: 0 <= k < arr.Length ==> maxVal >= arr[k]
    ensures exists k :: 0 <= k < arr.Length && maxVal == arr[k]
{
    maxVal := arr[0];
    var i := 1;
    while i < arr.Length
        invariant 1 <= i <= arr.Length
        invariant forall k :: 0 <= k < i ==> maxVal >= arr[k]
        invariant exists k :: 0 <= k < i && maxVal == arr[k]
    {
        if arr[i] > maxVal {
            maxVal := arr[i];
        }
        i := i + 1;
    }
}

Example 3: Class with Methods

Python Input:

class BankAccount:
    def __init__(self, balance):
        self.balance = balance

    def deposit(self, amount):
        self.balance += amount

    def withdraw(self, amount):
        if amount <= self.balance:
            self.balance -= amount
            return T