Automata, Languages and Compilers

Dafny

Paigaldamiseks on jälgi juhendit siit. NB! Seal on binaarfailide juhendist ainult vaja teha esimene samm, et .NET oleks paigaldatud. Ülejäänud teeb vscode ise.

Katsetamine

Kontrollime, kas installatsioon töötab...

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

method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
   // assert v == 3;
}

See peaks ilma hoiatusteta töötama. Proovi ka väljakommenteeritud osa tagasi panna. Järeltingimus ei ole piisavalt tugev, et seda leida. (Proovi lisada veel järeltingimus meetodile, et ta oskaks seda tõestada.)

Ülesanne 1

Leia eeltingimus järgmisele meetodile, et Dafny rahule jääks.

method Main(z: int) returns (y: int, x: int)
    ensures x == 2*y
{
    y := z + z;
    x := y * y;
}

Ülesanne 2

Lisa invariante, et tõestada järgmise programmi korrektsust.

method Mult(x: int, y: nat) returns (z: int)
  ensures z == x * y;
{
  var a := 0;
      z := 0;
  while a != y
  {
      z := z + x;
      a := a + 1;
  }
}

Ülesanne 3

Tõesta programmi MaxSectionSum korrektsus. See arvutab suurima alamjada summa Kadane algoritmi abil. Siin on Wikipedia kirjeldusega võrreldes "max" meetod otse if-lausetega realiseeritud --- võib pärast proovida Wikipediaga sarnasema koodi tõestamist.

function Sum(a: array<int>, m: int, n: int): int
  requires 0 <= m <= n <= a.Length
  reads a
{
  if (m==n) then 0 else Sum(a, m, n-1) + a[n-1]
}

method MaxSectionSum(a: array<int>) returns (s: int)
  ensures forall i,j :: 0 <= i <= j <= a.Length ==> Sum(a,i,j) <= s;
  ensures exists i,j :: 0 <= i <= j <= a.Length &&  s == Sum(a,i,j);
{
  s := 0;
  var k,t := 0,0;

  while (k < a.Length) 
  {
    t := t + a[k];
    k := k + 1;
    if t <= 0 {
      t := 0;
    } else if s < t {
      s := t;
    }
  }
}