1.A Dodatak: ispravnost

1.A.1 Primeri softverskih grešaka

Evo nekih od najpoznatijih i najzanimljivijih (pokušajte da na internetu pronađete još ovakvih primera):

1.A.2 Primeri dokazivanja korektnosti

U ovom poglavlju prikazaćemo još nekoliko primera dokaza korektnosti, što rekurzivnih, što iterativnih funkcija.

Minimum niza

Problem: Definisati funkciju koja određuje minimum nepraznog niza brojeva i dokazati njenu korektnost.

Algoritam se veoma jednostavno konstruiše induktivno-rekurzivnom konstrukcijom. Dimenzija problema u ovom primeru je broj elemenata niza.

Baza:

Ako niz ima samo jedan element, tada je taj element ujedno i minimum.

Korak:

U suprotnom, pretpostavimo da nekako umemo da rešimo problem za manju dimenziju i na osnovu toga pokušajmo da dobijemo rešenje za ceo niz. Dakle, pretpostavimo da je dužina niza \(n > 1\) i da umemo da nađemo broj \(m\) koji predstavlja minimum prvih \(n-1\) elemenata niza. Minimum celog niza dužine \(n\) je manji od brojeva \(m\) i preostalog, \(n\)-tog elementa niza (ako brojanje kreće od \(0\), to je element \(a_{n-1}\)).

Na osnovu ovoga možemo definisati rekurzivnu funkciju.

int minNiza(int a[], int n) {
    if (n == 1)
       return a[0];
    else {
       int m = minNiza(a, n-1);
       return min(m, a[n-1]);
    }
}

int main() {
    int a[] = {3, 5, 4, 1, 6, 2, 7};
    int n = 7;
    cout << minNiza(a, n) << endl;
}

Korektnost prethodnog algoritma se može formulisati u obliku sledeće teoreme.

Teorema 1.A.1. Za svaki neprazan niz \(a\) (niz za koji je dužina \(|a| \geq 1\)) i za svako \(1 \leq n \leq |a|\) poziv minNiza(a, n) vraća najmanji među prvih \(n\) elementa niza \(a\) (sa \(a\) i \(n\) su obeležene vrednosti niza a i promenljive n, a sa \(|a|\) dužina niza a).

Dokaz. Teoremu možemo dokazati indukcijom.

Dokažimo sada korektnost sledeće iterativne implementacije, korišćenjem tehnike invarijante petlje.

#include <iostream>
#include <algorithm>
using namespace std;

int minNiza(int[] a, int n) {
    int m = a[0];
    for (int i = 1; i < n; i++)
        m = min(m, a[i]);
    return m;
}

int main() {
    int a[] = {3, 5, 4, 1, 6, 2, 7};
    int n = 7;
    cout << minNiza(a, n) << endl;
}

U svakom koraku petlje, deo niza čiji minimum znamo postaje duži za po jedan element. Algoritam kreće od prefiksa niza dužine \(1\) i postavlja promenljivu m na vrednost prvog elementa niza \(a_0\). U svakom koraku petlje, pretpostavljamo da promenljiva m sadrži vrednost minimuma prvih \(i\) elemenata niza, a onda u telu petlje obrađeni deo niza proširujemo dodajući \(i+1\)-vi element niza, na poziciji \(i\). Minimum proširenog niza se izračunava kao minimum minimuma prvih \(i\) elemenata niza (čija je vrednost smeštena u promenljivoj m) i dodatnog elementa niza \(a_i\). Nakon izvršavanja tela petlje, deo niza čiji minimum je poznat je proširen na \(i+1\) element. Na kraju petlje je \(i\) jednako dužini niza, pa promenljiva m sadrži minimum celog niza.

Pre nego što pređemo na precizan dokaz prethodog razmatranja, skrenimo još jednom pažnju na to da imenovane veličine u matematici (tačnije algebri) i u programiranju imaju različite osobine. Naime, imenovane veličine u matematici (parametri, nepoznate) označavaju jednu vrednost, dok u (imperativnom) programiranju imenovane veličine imaju dinamički karakter i menjaju svoje vrednosti tokom izvršavanja programa po pravilima zadatim samim programom. Na primer, brojačka promenljiva i u nekoj petlji može redom imati vrednosti 1, 2 i 3. Prirodno je da tekuća vrednost promenljive i bude označena prosto sa \(i\). Međutim, nekada je važno da razlikujemo staru i novu vrednost promenljive i (vrednost pre i vrednost posle izvršavanja nekog koda), i tada ćemo koristiti oznake \(i'\) i \(i''\). Ako želimo da naglasimo da je promenljiva redom uzimala neku seriju vrednosti, koristićemo oznake \(i_0\) (početna vrednost promenljive i), \(i_1\), \(i_2\), … Vrednosti promenljivih koje koje se ne menjaju tokom izvršavanja programa ćemo označavati prosto imenom promenljive (npr. vrednost promenljive n iz prethodnog programa ćemo uvek označavati sa \(n\), a elemente niza a sa \(a_0\), \(a_1\), …, \(a_{n-1}\)).

Sledeću teoremu možemo strogo dokazati.

Teorema 1.A.2. Ako je niz \(a\) dužine \(n \geq 1\), neposredno pre početka petlje, u svakom koraku petlje (i na njenom početku, neposredno nakon provere uslova, ali i na njenom kraju, neposredno nakon izvršavanja tela), kao i nakon izvršavanja cele petlje važi da je \(1 \leq i \leq n\) i da je \(m\) minimum prvih \(i\) elemenata niza (gde je \(i\) tekuća vrednost promenljive i, a \(m\) tekuća vrednost promenljive m).

Dokaz. Ovo tvrđenje možemo dokazati indukcijom i to po broju izvršavanja tela petlje (obeležimo taj broj sa \(k\)). Napomenimo samo da ćemo petlju for smatrati samo skraćenicom za petlju while, tako da ćemo inicijalizaciju petlje smatrati za kôd koji se izvršava pre petlje, dok ćemo korak petlje smatrati kao poslednju naredbu tela petlje.

    int m = a[0];
    int i = 1;
    while (i < n) {
        m = min(m, a[i]);
        i++;
    }

Takođe, implicitno ćemo podrazumevati da se tokom izvršavanja petlje niz ni u jednom trenutku ne menja (i to se eksplicitno može dokazati indukcijom). Ni promenljiva n ne menja svoju vrednost.

Obeležimo sa \(m_0, m_1, \ldots, m_k, \ldots\) vrednosti promenljive m, a sa \(i_0, i_1, \ldots, i_k, \ldots\) vrednost promenljive i nakon \(0, 1, \ldots, k, \ldots\) izvršavanja tela petlje. Pošto promenljiva n ne menja svoju vrednost, njenu vrednost ćemo označiti sa \(n\).

Neka su \(i\) i \(m\) vrednosti promenljivih i i m nakon izvršavanja petlje. Na osnovu dokazanog tvrđenja znamo da uslovi navedeni u njemu važe i nakon završetka petlje. Kada se petlja završi, važi da je \(i = n\) (jer na osnovu prvog uslova znamo da je \(1 \leq i \leq n\), a uslov petlje i < n nije ispunjen). Na osnovu drugog uslova znamo da je \(m\) minimum \(n\) članova niza (što je zapravo ceo niz, jer je \(n\) njegova dužina), tj. da promenljiva m sadrži traženu vrednost, čime je dokazana parcijalna korektnost. Zaustavljanje se dokazuje jednostavno tako što se dokaže da se u svakom koraku petlje nenegativna vrednost \(n-i\) smanjuje za po 1, dok ne postane 0. \(\Box\)

Izolujmo ključne delove prethodnog dokaza i prikažimo ih u formatu koji ćemo i ubuduće koristiti prilikom dokazivanja invarijanti petlji (indukcija će u tim dokazima biti samo implicitna).

Lema 1.A.1. Ako je niz \(a\) dužine \(n \geq 1\), uslov da je \(1 \leq i \leq n\) i da je \(m\) minimum prvih \(i\) elemenata niza je invarijanta petlje (gde sa \(i\) obeležavamo tekuću vrednost promenljive i, a sa \(m\) tekuću vrednost promenljive m).

Dokaz. Dokažimo da invarijanta važi nakon inicijalizacije, a zatim i da se održava nakon izvršenja tela petlje.

Teorema 1.A.3. Nakon izvršavanja petlje, promenljiva m sadrži minimum celog niza.

Dokaz. Na osnovu invarijante važi da je \(1 \leq i \leq n\), a pošto po završetku petlje njen uslov nije ispunjen (ne važi \(i < n\)), važi da je \(i = n\). Na osnovu invarijante važi i da promenljiva m sadrži minimum prvih \(i\) elemenata niza, a pošto je \(i = n\), gde je \(n\) broj članova niza, to je zapravo minimum celog niza. \(\Box\)

Zadatak: Binarni zapis

Napiši program koji na osnovu neoznačenog celog broja \(n\) formira i ispisuje njegov 32-bitni binarni zapis.

Opis ulaza

Sa standardnog ulaza se unosi broj \(n\) (\(0 \leq n \leq 2^{32}-1\)).

Opis izlaza

Na standardni izlaz ispisati 32-bitni binarni zapis broja \(n\).

Primer 1
Ulaz
123456
Izlaz
00000000000000011110001001000000
Primer 2
Ulaz
16777215
Izlaz
00000000111111111111111111111111
Rešenje

Neka je niz od 32 logičke vrednosti popunjen vrednošću false. Binarni zapis određujemo tako što određujemo jednu po jednu binarnu cifru broja, zdesna nalevo. U svakom koraku petlje određujemo ostatak pri deljenju broja \(n\) sa \(2\), i na naredno mesto u nizu (u koraku \(i\) na mesto \(i\)) upisujemo true ako je taj ostatak jednak 1. Na kraju petlje, ispisujemo sadržaj niza unazad.

Primer 1.A.1. Prikažimo izvršavanje algoritma na primeru prevođenja broja 38 u binarni zapis. Prikazaćemo samo korake koji se izvode dok \(n\) ne postane 0 (od tog trenutka nadalje niz se samo popunjava nulama).

n      niz b
38
19       0
9       10
4      110
2     0110
1    00110
0   100110

Implementacija se može napraviti na sledeći način.

// broj koji se prevodi
unsigned long n;
cin >> n;

// niz binarnih cifara, redom, od cifre najmanje do
// cifre najvece tezine
bool binarneCifre[32] = {false};
// prevodjenje
for (int i = 0; n > 0; i++, n /= 2)
  binarneCifre[i] = n % 2;

// ispisujemo rezultat (od cifre najmanje tezine
for (int i = 31; i >= 0; i--)
  cout << (binarneCifre[i] ? '1' : '0');
cout << endl;
#include <iostream>

using namespace std;

int main() {
  // broj koji se prevodi
  unsigned long n;
  cin >> n;

  // niz binarnih cifara, redom, od cifre najmanje do
  // cifre najvece tezine
  bool binarneCifre[32] = {false};
  // prevodjenje
  for (int i = 0; n > 0; i++, n /= 2)
    binarneCifre[i] = n % 2;

  // ispisujemo rezultat (od cifre najmanje tezine
  for (int i = 31; i >= 0; i--)
    cout << (binarneCifre[i] ? '1' : '0');
  cout << endl;
  
  return 0;
}

Dokažimo korektnost ovog algoritma.

Da bismo lakše odredili invarijantu proširimo primer izvršavanja programa vrednošću binarnog broja trenutno zapisanog u nizu \(b\) i odgovarajućim stepenom dvojke.

n      niz b    b     2^i
38              0     1
19       0      0     2
9       10      2     4
4      110      6     8
2     0110      6    16
1    00110      6    32
0   100110     38    64

Sada se lako može primetiti da u svakom redu važi da je \(2^i\cdot n + b = 38\) (zaista, važi da je \(1\cdot 38 + 0\) = \(2 \cdot 19 + 0\) = \(4\cdot 9 + 2\) = \(8\cdot 4 + 6\) = \(16 \cdot 2 + 6\) = \(32 \cdot 1 + 6\) = \(64 \cdot 0 + 38 = 38\).

Lema 1.A.2. Uslov \(2^i \cdot n + b = n_0\) je invarijanta petlje, gde je \(b\) broj trenutno kodiran nizom binarnih cifara (ako logička vrednost na poziciji \(k\) u nizu odgovara cifri \(b_k\), neka je \(b = \sum_{k=0}^{31} b_k 2^k\)), gde je \(i\) tekuća vrednost promenljive i, dok je \(n_0\) početna, a \(n\) tekuća vrednost neoznačenog broja n.

Dokaz. Dokažimo da je navedeni uslov invarijanta.

Teorema 1.A.4. Po završetku algoritma niz sadrži binarni zapis neoznačenog broja n.

Dokaz. Kako je po izlasku iz petlje \(n=0\), na osnovu invarijante važi da je \(b = n_0\) tj. da niz sadrži binarni zapis polaznog broja. \(\Box\)

U narednom apletu možete videti korake u izvršavanju ovog algoritma i uveriti se da u svakom koraku invarijanta važi.

Zadatak: Najvredniji poklon

U prodavnici se nalazi \(n\) poklona, poređanih po ceni u rastućem redosledu. Svaki kupac želi da kupi što vredniji poklon, ali tako da ne prekorači svoj budžet.

Za svakog kupca potrebno je odrediti cenu najskupljeg poklona koji može da priušti.

Opis ulaza
Opis izlaza

Za svakog kupca ispisati po jedan ceo broj u zasebnom redu – cenu najskupljeg poklona koji je manji ili jednak od \(x_i\).

Ukoliko takav poklon ne postoji, ispisati \(-1\).

Primer
Ulaz
5
20 10 70 35 50
3
5 40 70
Izlaz
-1
35
70
Rešenje

Nakon što se niz cena sortira, zadatak se veoma efikasno može rešiti binarnom pretragom, primenjenu iznova na svaki budžet \(b_i\). Krenimo od sledeće invarijante. Tokom petlje održavaćemo dva pokazivača l i d, tako da su sve cene levo od pokazivača l takve da se poklon može kupiti za dati budžet, a sve cene desno od pokazivača d takve da se poklon ne može kupiti za dati budžet, dok su na pozicijama iz intervala \([l, d]\) cene koje algoritam još nije ispitao. Dakle, pretpostavimo da je stanje niza sledeće:

l d
\(\leq\) \(\leq\) \(\leq\) ? ? ? ? ? > > >

U početku su sve cene nepregledane, pa interval \([l, d]\) treba da se poklopi sa celim nizom, tj. \(l\) treba inicijalizovati na \(0\), a \(d\) na \(n-1\).

U svakom koraku petlje određujemo središnju poziciju \(s\) u intervalu \([l, d]\). Da bi se smanjila mogućnost prekoračenja, tu poziciju umesto pomoću \(\left\lfloor{\frac{l+d}{2}}\right\rfloor\), možemo izračunati pomoću \(l + \left\lfloor{\frac{d-l}{2}}\right\rfloor\).

Petlja se izvršava dok god ima nepregledanih cena, tj. dok je interval \([l, d]\) neprazan. Kada se pretraga završi, stanje u nizu je sledeće.

d l
\(\leq\) \(\leq\) \(\leq\) \(\leq\) \(\leq\) > > > > > >

Na osnovu invarijante znamo da se svaki element levo od \(l\) može priuštiti, a da se ni jedan desno od \(d\) ne može, pa se stoga traženi najvredniji poklon nalazi na poziciji \(d=l-1\). Ako su svi pokloni preskupi, krajnje vrednosti će biti \(d=-1\) i \(l=0\), pa se vraćanjem vrednosti \(d\) i u tom slučaju dobija korektan rezultat.

Funkcija se zaustavlja jer se u svakom koraku širina intervala \([l, d]\) striktno smanjuje (zahvaljujući zaokruživanju naniže prilikom određivanja središnje pozicije \(s\)).

// vraca poziciju u sortiranom nizu cene najvrednijeg poklona
// koji se moze kupiti za dati budzet ili
// -1 ako su svi pokloni preskupi
int najvredniji_poklon(const vector<int>& cene, int budzet) {
  int n = cene.size();
  int l = 0, d = n - 1;
  while (l <= d) {
    int s = l + (d - l) / 2;
    if (cene[s] <= budzet)
      l = s + 1;
    else
      d = s - 1;
  }
  return d;
}
#include <iostream>
#include <vector>
#include <algorithm>

using namespace std;

// vraca poziciju u sortiranom nizu cene najvrednijeg poklona
// koji se moze kupiti za dati budzet ili
// -1 ako su svi pokloni preskupi
int najvredniji_poklon(const vector<int>& cene, int budzet) {
  int n = cene.size();
  int l = 0, d = n - 1;
  while (l <= d) {
    int s = l + (d - l) / 2;
    if (cene[s] <= budzet)
      l = s + 1;
    else
      d = s - 1;
  }
  return d;
}

int main() {
  int n;
  cin >> n;
  vector<int> cene(n);
  for (int i = 0; i < n; i++)
    cin >> cene[i];
  sort(begin(cene), end(cene));
  int q;
  cin >> q;
  for (int i = 0; i < q; i++) {
    int budzet;
    cin >> budzet;
    int k = najvredniji_poklon(cene, budzet);
    if (k == -1)
      cout << -1 << endl;
    else
      cout << cene[k] << endl;
  }
  return 0;
}

1.A.3 Horova logika

Formalna specifikacija programa može se zadati u obliku Horove trojke. U tom slučaju preduslov opisuje uslove koji važe za ulazne promenljive, dok postuslov opisuje uslove koje bi trebalo da zadovolje rezultati izračunavanja. Na primer, program P za množenje brojeva \(x\) i \(y\), koji rezultat smešta u promenljivu \(z\) bi trebalo da zadovolji trojku \(\{\top\}\)P\(\{z = x\cdot y\}\) (\(\top\) označava iskaznu konstantu tačno, i ovom primeru znači da nema preduslova koje vrednosti \(x\) i \(y\) treba da zadovoljavaju). Ako se zadovoljimo time da program može da množi samo nenegativne brojeve, specifikacija se može oslabiti u \(\{x \geq 0\ \wedge\ y \geq 0\}\)P\(\{z = x\cdot y\}\).

Jedno od ključnih pitanja za verifikaciju je pitanje da li je neka Horova trojka tačna (tj. da li program zadovoljava datu specifikaciju). Hor je dao formalni sistem (aksiome i pravila izvođenja) koji omogućava da se tačnost Horovih trojki dokaže na formalan način (slika @fig:horov_sistem). Za svaku sintaksnu konstrukciju programskog jezika koji se razmatra formiraju se aksiome i pravila izvođenja koji daju rigorozan opis semantike odgovarajućeg konstrukta programskog jezika.2

Opis aksiome i pravila Horove logike:

Dokazi ispravnosti programa u okviru Horove logike koriste instance aksioma (aksiome primenjene na neke konkretne naredbe) i iz njih, primenom pravila, izvode nove zaključke. Dokazi se mogu pogodno prikazati u vidu stabla, u čijem su listovima primene aksioma.

Stepenovanje

Dokažimo korektnost algoritma stepenovanja. Potrebno je dokazati sledeću trojku.

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0\}\\ \mathtt{i:=0;\ s:=1;\ while\ (i < k)\ do\ begin\ s := s * x;\ i := i+1\ end}\\ \{s = x^k\} \end{array} \]

Na osnovu pravila dodele primenjenog na dodele i:=0 i m:=0 i dva puta primenjenog pravila kompozicije važi trojka

\[\{x > 0 \wedge k \geq 0\}\mathtt{i:=0;\ s:=1}\{x > 0 \wedge k \geq 0 \wedge i = 0 \wedge s = 1\}\]

Dovoljno je, dakle, da dokažemo trojku

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge i = 0 \wedge s = 1\}\\ \mathtt{while\ (i < k)\ do\ begin\ s := s * x;\ i := i+1\ end}\\ \{s = x^k\} \end{array} \]

Primenimo pravilo petlje na ovu petlju uz invarijantu \(\varphi \equiv x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\). Potrebno je dokazati da telo petlje čuva invarijantu tj. dokazati trojku:

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i \wedge i < k\}\\ \mathtt{m := m * x;\ i := i+1}\\ \{x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\} \end{array} \]

tj. \[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge 0 \leq i < k \wedge m = x^i\}\\ \mathtt{m := m * x;\ i := i+1}\\ \{x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\} \end{array} \]

Nakon prve dodele, na osnovu pravila dodele, važi trojka

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge 0 \leq i < k \wedge m = x^i\}\\ \mathtt{m := m * x}\\ \{x > 0 \wedge k \geq 0 \wedge 0 \leq i < k \wedge m = x^{i+1}\} \end{array} \]

Zaista, zamenom promenljive \(m\) izrazom \(m\cdot x\) u postuslovu i skraćivanjem vrednosti \(x\) (što je dopušteno, jer važi \(x > 0\)) dobija se tačno preduslov.

Nakon druge dodele, na osnovu pravila dodele važi trojka

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge 0 \leq i < k \wedge m = x^{i+1}\}\\ \mathtt{i := i + 1}\\ \{x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\} \end{array} \]

Zaista, zamenom vrednosti \(i\) sa \(i+1\) u postuslovu dobija se uslov \(x > 0 \wedge k \geq 0 \wedge 0 \leq i+1 \leq k \wedge m = x^{i+1}\), koji je logička posledica preduslova. Dakle, kombinovanjem pravila posledice i pravila kompozicije dobija se trojka koja garantuje da telo petlje zadovoljava invarijantu, odakle, na osnovu pravila petlje, sledi trojka

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\}\\ \mathtt{while\ (i < k)\ do\ begin\ m := m * x;\ i := i+1\ end}\\ \{x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i \wedge i \geq k\} \end{array} \]

Postuslov implicira \(i=k\), pa zato i željeni uslov \(m = x^k\). Ostalo je još da se prethodna trojka spoji sa trojkom

\[ \{x > 0 \wedge k \geq 0\} \mathtt{i:=0;\ m:=1} \{x > 0 \wedge k \geq 0 \wedge i = 0 \wedge m = 1\} \]

koju smo ranije dokazali. Za to je dovoljno primetiti da uslov \(x > 0 \wedge k \geq 0 \wedge i = 0 \wedge m = 1\) povlači uslov invarijante \(x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\). Zato se trojka koja zaključak pravila petlje, na osnovu pravila posledice, može zameniti željenom trojkom:

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0 \wedge i = 0 \wedge m = 1\}\\ \mathtt{while\ (i < k)\ do\ begin\ m := m * x;\ i := i+1\ end}\\ \{m = x^k\} \end{array} \]

Sada na osnovu pravila kompozicije sledi korektnost celog algoritma tj. trojka:

\[ \begin{array}{l} \{x > 0 \wedge k \geq 0\}\\ \mathtt{i:=0;\ m:=1;\ while\ (i < k)\ do\ begin\ m := m * x;\ i := i+1\ end}\\ \{m = x^k\} \end{array} \]

1.A.4 Softver za dokazivanje korektnosti programa

Verifikacija softvera je razvijena oblast i postoji određen broj softverskih sistema koji se koriste za verifikaciju softvera. Samo ilustrativno, da bi se stekao neki osećaj kako se ovaj alat koristi navešćemo dva primera.

Softver Dafny (https://dafny.org/) je razvijen u kompaniji Microsoft. Program se piše na posebnom jeziku koji pored naredbi sadrži i specifikaciju (preduslove, postuslove, invarijante). Ako automatski dokazivač uspe da dokaže sve uslove koje je programer naveo, moguće je izvesti izvorni kod u nekom od klasičnih programskih jezika (Java, C#, …).

U narednom kodu je prikazana funkcija za izračunavanje maksimuma niza. Kao preduslov (klauzula requires) navedeno je da niz mora biti neprazan, a kao postusplov (klauzule ensures) navedeno je da je povratna vrednost max zaista maksimum niza (veća je ili jednaka od svih članova niza i javlja se u nizu). Uz petlju je navedena i invarijanta koja tvrdi da se brojač i petlje uvek nalazi u granicama \([1, n]\), gde je \(n\) dužina niza i da u svakom koraku petlje promenljiva max sadrži maksimum prvih i članova niza. Da bi se automatski moglo dokazati zaustavljanje, formulisana je i varijanta koja kaže da se u svakom koraku petlje vrednost \(n-i\) smanjuje. Ova specifikacija je dovoljna da bi softver Dafny dokazao korektnost algoritma određivanja maksimuma niza i njegove implementacije.

// 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
  // max je najveći element niza
  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
     // (nakon petlje i će biti jednako dužini niza arr)
     invariant 1 <= i <= arr.Length
     // 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;
  }
}

  1. Osnovna razlika između računarskog virusa i računarskog crva je u tome što virus mora biti aktiviran nekakvom akcijom na računaru na kojem se nalazi. S druge strane, crv je samostalni program koji može da se replicira i širi čim dopre do nekog računarskog sistema.↩︎

  2. U svom originalnom radu, Hor je razmatrao veoma jednostavan programski jezik (koji ima samo naredbu dodele, naredbu grananja, jednu petlju i sekvencijalnu kompoziciju naredbi), ali u nizu radova drugih autora Horov originalni sistem je proširen pravilima za složenije konstrukte programskih jezika (funkcije, pokazivače, itd.).↩︎