Software🔗

This course will make use of the following software:

• Operating system: macOS, Windows, or Linux

• Dafny: the implementation language and source language of our compilers.

• Python langs package: a package containing utilities for this course.

Instruction for using each system are below:

• Dafny

• Python

1 Dafny🔗

Dafny is a “verification-aware” object-oriented programming language that we will be using in this class. This page contains installation information for both the Dafny tools and interactive-development-environment (IDE) support, links to resources you may find useful, and explanations for how to run Dafny once it is installed.

1.1 Installation🔗

We recommend using VS Code with Dafny extension as your IDE. Follow the Official Installation Instructions To test your installation, open a new file, and copy/paste the following code:

hello-world.dfy

method Main(){

print "hello, world\n";

}

If everything is installed correctly, VS Code will display a green checkmark to the left of the method name.

2 Python🔗

3 Rocq🔗

https://rocq-prover.org/install#mac-vscode

4 Other Resources🔗

• Getting Started (Tutorial)

• Quick Reference

• Language Reference Manual

• Style Guide

• Dafny Documentation

• AWS Dafny training lecture slides and Exercises

• SAT/SMT by Example

• Z3 API in Python