Language

• mypy
• python subset + types
• specifications: res
• The specification language is designed to match Dafny's as closely as possible and can be viewed here:

Typing Requirements

dafny-of-python requires program to be well-typed as enforced by the Mypy typechecker. This includes complete type annotations to be specified for functions, in accordance with PEP 484. As Dafny is a statically typed language, this information is directly used in the translation and is crucial for emitting valid Dafny programs.

This introduces the following differences from regular Python program:

• Variables can only have single type throughout the program, unless they are redeclared
• Lists are homogenous, supporting elements of only a single type. This does not include tuples, which can be polymorphic.

Grammar

Based on https://docs.python.org/3/reference/grammar.html