python-to-dafny-translator
Installation
SKILL.md
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
| Python has | Dafny needs | You must supply |
|---|---|---|
| Duck typing | Static types | Type annotations — infer from usage if not annotated |
Unbounded int |
Unbounded int — ✅ matches |
Nothing. This is the easy one. |
list (mutable, heterogeneous) |
seq<T> (immutable, homogeneous) or array<T> (mutable, heap) |
Choose: algorithm is functional → seq. Mutates in place → array + frame conditions. |
dict |
map<K,V> (immutable) |
Usually fine — most dict uses are read-mostly |
for x in xs |
`while i < | xs |
| Exceptions | No exceptions | Encode as Result datatype, or as a precondition that rules out the failing case |
| Implicit termination | Explicit decreases clause |
Find the measure — usually the loop bound or recursion arg size |
| No spec | requires/ensures |
The hard part. See below. |