Language

The source language is composed of a subset of typed Python along with specification constructs based on the Dafny language.

Here is the complete grammar currently supported

It is based on https://docs.python.org/3/reference/grammar.html

Python Subset

dafny-of-python implements support for functions, conditionals, lambda functions, while loops, ternary expressions, lists and tuples. Notably, the following are supported by Dafny and can be included in the future:

• classes
• generator functions
• comprehensions
• operator chaining
• sets
• dictionaries

Tuples with a single element are translated to the element itself in Dafny. The use of Dafny imposes a few restrictions on constructs that are otherwise supported in Python. The following are hence not supported by dafny-of-python.

• for loops
• continue statements
• non-call expressions as statements

Indentation

The only form of indentation currently supported is using 2 space characters.

Lists

Primitive operations, such as + and updates (eg. XS[0] = 10) are not yet supported.

Built-Ins

• map
• filter

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.

Specifications

dafny-of-python introduces specification constructs for programs to be verified. For simplicity, these do not deviate from their equivalents in Dafny. Additionally, in order to enable the Python programs to remain executable without modification, the specification constructs are supported via single line comments which immediately precede the language constructs for which they are used. An excellent tutorial covering these specification constructs is provided at MSR Dafny Tutorial.

The following specification constructs are supported by dafny-of-python:

Specification Construct	Construct(s) To Use With	Purpose
precondition	function	conditions that must hold when the function is called
postcondition	function	conditions that must hold after the function has executed
reads clause	function, while loop	memory locations allowed to read
modifies clause	function, while loop	memory locations allowed to modify
decreases clause	function, while loop	expression which decreases, to ensure termination
invariant	while loop	condition that holds at every iteration of the loop

Reserved Keywords

• res: name for the result parameter of every method