Implementation

Main stages in going from program to verification result:

annotated program 
-> type checking with Mypy -> parsing with OCamllex and Menhir
-> operations on Python AST -> translation to Dafny AST -> printing of Dafny AST 
-> running verifier -> reporting results

Lists

Supporting lists has the following requirements:

• Mutability
• Methods, such as append
• Primitive operations, such as + which is used to concatenate two lists

While Dafny supports arrays which are mutable, their operations do not correspond to lists in Python. As such, lists are supported via the following:

1. a list class specified in Dafny
2. rewriting lists to make use of the specified list class Currently, lists are the only mutable data structure supported. Support for other data structures can be added in a similar manner.

Here is the complete list specification

List Class

The list class specifies a generic parameter for its elements and internally makes use of a sequence to store them. It supports all methods of Python’s list class except for sort. In the case of sort, since the elements are of a generic type, a general comparison function cannot be used. Where possible, preconditions are specified in order to restrict the possible uses. For instance, the pop method specifies that the length of the list should be greater than one so that a verification will be raised if it is not:

method pop() returns (popped: T)
  requires |lst| > 0
  modifies this
  ensures lst == old(lst)[0..|old(lst)| - 1] ensures popped == old(lst)[|old(lst)| - 1]
{
  popped := lst[|lst| - 1];
  lst := lst[0..|lst| - 1]; 
}

Rewriting Lists

In rewriting Python lists to correspond to the Dafny list class, the following operations are performed:

1. for every literal list such as [1, 2, 3], an assignment statement is created whose right-hand expression is a call to the list constructor. The literal list is then replaced with the assignment’s identifier
2. subscripts are converted to their corresponding to method call in the list class [0..3] would be converted to .range(0, 3)
3. the Python built-in function len is converted to the len method of the list class. len([1, 2, 3]) would be converted to [1, 2, 3].len().

Primitive Operations

To extend primitive operation support for datastructures, type inference can be used to recognize recognize these operations involving datastructures and rewrite them accordingly. This remains to be implemented.

Built-Ins

Together with the translated user program, a set of functions specified in Dafny is also appended before the Dafny verifier is executed. These functions correspond to built-in functions in Python and enables them to be incorporated as part of the verification process. Currently, map and filter are supported.

Here are the built-in specifications