Tools

Gaubao

Guabao is a programming environment encouraging the methodology that a program and its correctness proof should be developed hand in hand, and that how a program should be proved could sometimes give hints how the program can be written.

It is still under development and unfortunately not yet ready for this course. For more info, see the project page.

Dafny

From its homepage:

Dafny is a verification-aware programming language that has native support for recording specifications and is equipped with a static program verifier. By blending sophisticated automated reasoning with familiar programming idioms and tools, Dafny empowers developers to write provably correct code (w.r.t. specifications). It also compiles Dafny code to familiar development environments such as C#, Java, JavaScript, Go and Python (with more to come) so Dafny can integrate with your existing workflow. Dafny makes rigorous verification an integral part of development, thus reducing costly late-stage bugs that may be missed by testing.

Dafny is a very matured system, and its philosophy is very relevant to our course. Students are encouraged to give it a try.