Dafny Introduction

• Readings
  • Recommended readings
• Topics
• Example: Absolute value

Readings

• Sections 1-5 of [Koen12], an introduction to the Dafny language
  • Also available as an online tutorial
• Examples
• Dafny Reference Manual

Recommended readings

• [Wing95], which provides several hints to specifiers.

Topics

• Specifying and verifying programs in high-level programming languages.
• Introduction to Dafny. Main features.
• Method contracts in Dafny.
• Specifying pre and post-conditions.
• Compositional verification of methods through the use of contracts.

Example: Absolute value

method abs (x : int) returns (y : int)
    ensures 0 <= x ==> x == y
    ensures 0 > x ==> -x == y
{
    if x < 0
    {
        return -x;
    }
    else
    {
        return x;
    }
}

method Main()
{
    var x := -3;
    var n := abs(x);
    assert n >= 0;
    print "Absolute value of ", x, ": ", n, "\n";
}