-
Notifications
You must be signed in to change notification settings - Fork 1
Limitations
dafny-of-python has some notable limitations, primarily due to relying on Dafny as the sole underlying verifier.
There is no formal proof that the semantics of the program are preserved during translation. As such, inaccurate translations may occur, which may have to be modified through manual inspection of the output Dafny program.
Debugging support is limited. In the case of a verification error, the user’s only option is to iteratively modify and invoke the verifier. While there is support for obtaining a counterexample through Dafny's VS Code extension, this is not available through its commandline interface. Ideally, dafny-of-python would also enable the user to understand the root cause of errors and provide example scenarios leading to the errors.
The following constructs are not supported:
- continue statements
- non-call expressions as statements
- tuples with a single element
The specification constructs provided by Dafny may not be expressive enough in practice in order to capture the requirements of a program. For example, a program may verify without errors when implementing quicksort even though mergesort is required.
Dafny does not support verification of concurrent programs.