Dafny Blog Snippets

basic-types.dfy

type Timestamp = t: int| 0 <= t <= 9223372036854775808 //2^63

class Entity
{
    var id : string

    predicate isEqual(other : Entity)
        reads this, other
    {
        id == other.id
    }
}

syntax-example.dfy

method sumAndZero(arr: array<int>) returns (sum: nat)
  requires forall i :: 0 <= i < arr.Length  ==>  arr[i] >= 0
  modifies arr
{
  var i: int := 0;
  sum := 0;
  //
  while(i < arr.Length) {
    sum := sum + arr[i];
    arr[i] := arr[i];
    i := i + 1;
  }
}