+++
title = "Dafny"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3d"]
forwardlinks = ["3d2"]
zettelid = "3d1"
+++

Dafny is a tool that was created by Runstan Lino, which is a language
that was designed specifically for the purposes of verification. The
main idea is that you can have preconditions and postconditions that
describe the functionality of your program. These are then proven
automatically by dafny, which uses the implementation to try and prove
the postcondition assuming that the precondition holds.

This cannot always be the case though, and one can therefore help the
theorem prover by adding assertions in different places.