Алат за испитивање коректности софтвера

Верификација софтвера је развијена област и постоји одређен број софтверских система који се користе за верификацију софтвера. Само илустративно, да би се стекао неки осећај како се овај алат користи навешћемо два примера.

Софтвер Dafny (https://dafny.org/) је развијен у компанији Microsoft. Програм се пише на посебном језику који поред наредби садржи и спецификацију (предуслове, постуслове, инваријанте). Ако аутоматски доказивач успе да докаже све услове које је програмер навео, могуће је извести изворни код у неком од класичних програмских језика (Java, C#, …).

У наредном коду је приказана функција за израчунавање максимума низа. Као предуслов (клаузула requires) наведено је да низ мора бити непразан, а као постусплов (клаузуле ensures) наведено је да је повратна вредност max заиста максимум низа (већа је или једнака од свих чланова низа и јавља се у низу). Уз петљу је наведена и инваријанта која тврди да се бројач i петље увек налази у границама \([1, n]\), где је \(n\) дужина низа и да у сваком кораку петље променљива max садржи максимум првих i чланова низа. Да би се аутоматски могло доказати заустављање, формулисана је и варијанта која каже да се у сваком кораку петље вредност \(n-i\) смањује.

// metod Max izračunava najveći element datog nepraznog niza arr
method Max(arr: array<int>) returns (max: int)
  // maksimum računamo samo za neprazne nizove
  requires arr.Length > 0
  // naredna dva svojstva obezbeđuju da je max najveći element niza arr
  ensures forall j :: 0 <= j < arr.Length ==> max >= arr[j]
  ensures exists j :: 0 <= j < arr.Length && max == arr[j]
{
  max := arr[0];
  var i: int := 1;
  while (i < arr.Length)
     // granice promenljive i (ovim se obezbedjuje da je nakon petlje
     // i jednako dužini niza arr
     invariant 1 <= i <= arr.Length
     // naredna invarijanta tvrdi da promenljiva max sadrži najveću
     // vrednost prvih i elemenata niza
     invariant forall j :: j >= 0 && j < i ==> max >= arr[j]
     invariant exists j :: j >= 0 && j < i && max == arr[j]
     // naredna varijanta obezbeđuje zaustavljanje (ova razlika se
     // smanjuje sve dok ne dođe do nule)
     decreases arr.Length - i
  {
    if (arr[i] >= max) 
    {
      max := arr[i];
    }
    i := i + 1;
  }
}

Поред аутоматских доказивача теорема, за верификацију се често користе и интерактивни доказивачи теорема. У наставку је приказана рекурзивна имплементација функције за одређивање максимума у функционалном језику интерактивног доказивача Isabelle/HOL (https://isabelle.in.tum.de/). Излаз из рекурзије представља случај једночлане листе и тада је максимум једнак том једном елементу. Рекурзивни корак представља листа која се добије надовезивањем једног елемента x на реп листе xs и тада се резултат добије одређивањем максимума вредности x и рекурзивно израчунатог максимума репа листе xs. Након дефиниције функције следе леме које говоре о коректности ове функције. Прва лема је помоћна и говори да се рекурзивно правило може применити када год је реп непразан. Након тога следи централна лема која говори да је у случају непразне листе добијена вредност максимума већа или једнака од свих елемената листе, као и да она припада скупу елемената листе. Након сваке леме написани су и докази на специјализованом језику који овај интерактивни доказивач разуме.

fun max_list :: "nat list ⇒ nat" where
  "max_list [x] = x"
| "max_list (x # xs) = max x (max_list xs)"

lemma max_list_Cons [simp]:
  assumes "xs ≠ []"
  shows "max_list (x # xs) = max x (max_list xs)"
  using assms
  by (metis max_list.elims max_list.simps(2))

lemma 
  assumes "xs ≠ []"
  shows "∀ x ∈ set xs. max_list xs ≥ x ∧ max_list xs ∈ set xs"
  using assms
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  show ?case
  proof (cases "xs = []")
    case True
    then show ?thesis by simp
  next
    case False
    with Cons show ?thesis by auto linarith
  qed
qed