Dafny is an open source programming language created in 2009 by K. Rustan M. Leino.
#211on PLDB | 15Years Old | 157Repos |
git clone https://github.com/Microsoft/dafny
Dafny is an imperative compiled language that targets C# and supports formal specification through preconditions, postconditions, loop invariants and loop variants. The language combines ideas primarily from the Functional and Imperative paradigms, and includes limited support for Object-Oriented Programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Read more on Wikipedia...
method Main() {
print "Hello, world!\n";
}
// Hello world in Dafny
method Main() {
print "Hello, World!\n";
}
datatype List = Nil | Link(data:int,next:List)
function sum(l:List): int {
match l
case Nil => 0
case Link(d,n) => d + sum(n)
}
predicate isNatList(l:List) {
match l
case Nil => true
case Link(d,n) => d >= 0 && isNatList(n)
}
ghost method NatSumLemma(l:List, n:int)
requires isNatList(l) && n == sum(l)
ensures n >= 0
{
match l
case Nil =>
// Discharged Automatically
case Link(data,next) => {
// Apply Inductive Hypothesis
NatSumLemma(next,sum(next));
// Check what known by Dafny
assert data >= 0;
}
}
Feature | Supported | Example | Token |
---|---|---|---|
Print() Debugging | ✓ | ||
Comments | ✓ | // A comment | |
Line Comments | ✓ | // A comment | // |
Semantic Indentation | X |