Python → Dafny Translator

Dafny is a verification-aware language: you write code + spec together, and the verifier checks the code meets the spec. Translating from Python means adding everything Dafny needs that Python omits: types, termination measures, loop invariants, and a precise contract.

The impedance mismatch

Step 1 — Extract the spec

The contract has to come from somewhere. In priority order:

1. Docstring says what the function returns → that's your ensures.
2. Function name is a known algorithm (binary_search, sort, gcd) → use the textbook postcondition.
3. Assertions in the code → promote to ensures/requires.
4. Test cases → each test is a ground instance; generalize.
5. Nothing → ask the user. You can't verify against an unknown spec.

Step 2 — Translate the body

Step 3 — Add invariants (the hard part)

Every while needs invariants strong enough that invariant ∧ ¬guard ⟹ postcondition.

Pattern — accumulator loops: The invariant says "the accumulator holds the result for the prefix processed so far."

// Python: total = sum(xs)
var i, total := 0, 0;
while i < |xs|
  invariant 0 <= i <= |xs|
  invariant total == Sum(xs[..i])     // "correct so far"
  decreases |xs| - i
{ total := total + xs[i]; i := i + 1; }

Pattern — search loops: The invariant says "the thing isn't in the part we've already looked at."

Pattern — two-pointer: Two index-bound invariants plus the relationship between them.

If you can't find the invariant: → invariant-inference.

Worked example

Python:

def index_of(xs: list[int], target: int) -> int:
    """Return index of target in xs, or -1."""
    for i, x in enumerate(xs):
        if x == target:
            return i
    return -1

Dafny:

method IndexOf(xs: seq<int>, target: int) returns (r: int)
  ensures r == -1 ==> target !in xs
  ensures r >= 0  ==> 0 <= r < |xs| && xs[r] == target
{
  var i := 0;
  while i < |xs|
    invariant 0 <= i <= |xs|
    invariant target !in xs[..i]      // not found in the prefix
    decreases |xs| - i
  {
    if xs[i] == target { return i; }
    i := i + 1;
  }
  return -1;
}

Verifies. The target !in xs[..i] invariant plus loop exit (i == |xs|) gives target !in xs, which discharges the r == -1 postcondition.

What doesn't translate

Flag these. A translation with assume false hidden where the hard part is is worse than no translation.

Do not

• Do not weaken the postcondition until it verifies. ensures true always verifies and proves nothing.
• Do not use assume to paper over a hard invariant. assume is a trust hole — mark it LOUDLY and justify it.
• Do not translate the bug. If the Python has an off-by-one, Dafny will refuse to verify — good. Don't "fix" the spec to match the bug.
• Do not skip the termination clause. Dafny requires it; decreases * means "I gave up on proving this terminates" — only acceptable if the function genuinely might not.

Output format

## Spec (extracted from)
<docstring | algorithm name | tests | user-provided>

## Dafny
<code block — must verify clean or failures must be annotated>

## Trust holes
<every `assume` with justification, or "none">

## Untranslated
<Python constructs with no Dafny equivalent — and what you did instead>