1.A Додатак: исправност

1.A.1 Примери софтверских грешака

Ево неких од најпознатијих и најзанимљивијих (покушајте да на интернету пронађете још оваквих примера):

1.A.2 Примери доказивања коректности

У овом поглављу приказаћемо још неколико примера доказа коректности, што рекурзивних, што итеративних функција.

Минимум низа

Проблем: Дефинисати функцију која одређује минимум непразног низа бројева и доказати њену коректност.

Алгоритам се веома једноставно конструише индуктивно-рекурзивном конструкцијом. Димензија проблема у овом примеру је број елемената низа.

База:

Ако низ има само један елемент, тада је тај елемент уједно и минимум.

Корак:

У супротном, претпоставимо да некако умемо да решимо проблем за мању димензију и на основу тога покушајмо да добијемо решење за цео низ. Дакле, претпоставимо да је дужина низа \(n > 1\) и да умемо да нађемо број \(m\) који представља минимум првих \(n-1\) елемената низа. Минимум целог низа дужине \(n\) је мањи од бројева \(m\) и преосталог, \(n\)-тог елемента низа (ако бројање креће од \(0\), то је елемент \(a_{n-1}\)).

На основу овога можемо дефинисати рекурзивну функцију.

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;
}

Коректност претходног алгоритма се може формулисати у облику следеће теореме.

Теорема 1.A.1. За сваки непразан низ \(a\) (низ за који је дужина \(|a| \geq 1\)) и за свако \(1 \leq n \leq |a|\) позив minNiza(a, n) враћа најмањи међу првих \(n\) елемента низа \(a\) (са \(a\) и \(n\) су обележене вредности низа a и променљиве n, а са \(|a|\) дужина низа a).

Доказ. Теорему можемо доказати индукцијом.

Докажимо сада коректност следеће итеративне имплементације, коришћењем технике инваријанте петље.

#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;
}

У сваком кораку петље, део низа чији минимум знамо постаје дужи за по један елемент. Алгоритам креће од префикса низа дужине \(1\) и поставља променљиву m на вредност првог елемента низа \(a_0\). У сваком кораку петље, претпостављамо да променљива m садржи вредност минимума првих \(i\) елемената низа, а онда у телу петље обрађени део низа проширујемо додајући \(i+1\)-ви елемент низа, на позицији \(i\). Минимум проширеног низа се израчунава као минимум минимума првих \(i\) елемената низа (чија је вредност смештена у променљивој m) и додатног елемента низа \(a_i\). Након извршавања тела петље, део низа чији минимум је познат је проширен на \(i+1\) елемент. На крају петље је \(i\) једнако дужини низа, па променљива m садржи минимум целог низа.

Пре него што пређемо на прецизан доказ претходог разматрања, скренимо још једном пажњу на то да именоване величине у математици (тачније алгебри) и у програмирању имају различите особине. Наиме, именоване величине у математици (параметри, непознате) означавају једну вредност, док у (императивном) програмирању именоване величине имају динамички карактер и мењају своје вредности током извршавања програма по правилима задатим самим програмом. На пример, бројачка променљива i у некој петљи може редом имати вредности 1, 2 и 3. Природно је да текућа вредност променљиве i буде означена просто са \(i\). Међутим, некада је важно да разликујемо стару и нову вредност променљиве i (вредност пре и вредност после извршавања неког кода), и тада ћемо користити ознаке \(i'\) и \(i''\). Ако желимо да нагласимо да је променљива редом узимала неку серију вредности, користићемо ознаке \(i_0\) (почетна вредност променљиве i), \(i_1\), \(i_2\), … Вредности променљивих које које се не мењају током извршавања програма ћемо означавати просто именом променљиве (нпр. вредност променљиве n из претходног програма ћемо увек означавати са \(n\), а елементе низа a са \(a_0\), \(a_1\), …, \(a_{n-1}\)).

Следећу теорему можемо строго доказати.

Теорема 1.A.2. Ако је низ \(a\) дужине \(n \geq 1\), непосредно пре почетка петље, у сваком кораку петље (и на њеном почетку, непосредно након провере услова, али и на њеном крају, непосредно након извршавања тела), као и након извршавања целе петље важи да је \(1 \leq i \leq n\) и да је \(m\) минимум првих \(i\) елемената низа (где је \(i\) текућа вредност променљиве i, а \(m\) текућа вредност променљиве m).

Доказ. Ово тврђење можемо доказати индукцијом и то по броју извршавања тела петље (обележимо тај број са \(k\)). Напоменимо само да ћемо петљу for сматрати само скраћеницом за петљу while, тако да ћемо иницијализацију петље сматрати за кôд који се извршава пре петље, док ћемо корак петље сматрати као последњу наредбу тела петље.

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

Такође, имплицитно ћемо подразумевати да се током извршавања петље низ ни у једном тренутку не мења (и то се експлицитно може доказати индукцијом). Ни променљива n не мења своју вредност.

Обележимо са \(m_0, m_1, \ldots, m_k, \ldots\) вредности променљиве m, а са \(i_0, i_1, \ldots, i_k, \ldots\) вредност променљиве i након \(0, 1, \ldots, k, \ldots\) извршавања тела петље. Пошто променљива n не мења своју вредност, њену вредност ћемо означити са \(n\).

Нека су \(i\) и \(m\) вредности променљивих i и m након извршавања петље. На основу доказаног тврђења знамо да услови наведени у њему важе и након завршетка петље. Када се петља заврши, важи да је \(i = n\) (јер на основу првог услова знамо да је \(1 \leq i \leq n\), а услов петље i < n није испуњен). На основу другог услова знамо да је \(m\) минимум \(n\) чланова низа (што је заправо цео низ, јер је \(n\) његова дужина), тј. да променљива m садржи тражену вредност, чиме је доказана парцијална коректност. Заустављање се доказује једноставно тако што се докаже да се у сваком кораку петље ненегативна вредност \(n-i\) смањује за по 1, док не постане 0. \(\Box\)

Изолујмо кључне делове претходног доказа и прикажимо их у формату који ћемо и убудуће користити приликом доказивања инваријанти петљи (индукција ће у тим доказима бити само имплицитна).

Лема 1.A.1. Ако је низ \(a\) дужине \(n \geq 1\), услов да је \(1 \leq i \leq n\) и да је \(m\) минимум првих \(i\) елемената низа је инваријанта петље (где са \(i\) обележавамо текућу вредност променљиве i, а са \(m\) текућу вредност променљиве m).

Доказ. Докажимо да инваријанта важи након иницијализације, а затим и да се одржава након извршења тела петље.

Теорема 1.A.3. Након извршавања петље, променљива m садржи минимум целог низа.

Доказ. На основу инваријанте важи да је \(1 \leq i \leq n\), а пошто по завршетку петље њен услов није испуњен (не важи \(i < n\)), важи да је \(i = n\). На основу инваријанте важи и да променљива m садржи минимум првих \(i\) елемената низа, а пошто је \(i = n\), где је \(n\) број чланова низа, то је заправо минимум целог низа. \(\Box\)

Задатак: Бинарни запис

Напиши програм који на основу неозначеног целог броја \(n\) формира и исписује његов 32-битни бинарни запис.

Опис улаза

Са стандардног улаза се уноси број \(n\) (\(0 \leq n \leq 2^{32}-1\)).

Опис излаза

На стандардни излаз исписати 32-битни бинарни запис броја \(n\).

Пример 1
Улаз
123456
Излаз
00000000000000011110001001000000
Пример 2
Улаз
16777215
Излаз
00000000111111111111111111111111
Решење

Нека је низ од 32 логичке вредности попуњен вредношћу false. Бинарни запис одређујемо тако што одређујемо једну по једну бинарну цифру броја, здесна налево. У сваком кораку петље одређујемо остатак при дељењу броја \(n\) са \(2\), и на наредно место у низу (у кораку \(i\) на место \(i\)) уписујемо true ако је тај остатак једнак 1. На крају петље, исписујемо садржај низа уназад.

Пример 1.A.1. Прикажимо извршавање алгоритма на примеру превођења броја 38 у бинарни запис. Приказаћемо само кораке који се изводе док \(n\) не постане 0 (од тог тренутка надаље низ се само попуњава нулама).

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

Имплементација се може направити на следећи начин.

// 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;
}

Докажимо коректност овог алгоритма.

Да бисмо лакше одредили инваријанту проширимо пример извршавања програма вредношћу бинарног броја тренутно записаног у низу \(b\) и одговарајућим степеном двојке.

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

Сада се лако може приметити да у сваком реду важи да је \(2^i\cdot n + b = 38\) (заиста, важи да је \(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\).

Лема 1.A.2. Услов \(2^i \cdot n + b = n_0\) је инваријанта петље, где је \(b\) број тренутно кодиран низом бинарних цифара (ако логичка вредност на позицији \(k\) у низу одговара цифри \(b_k\), нека је \(b = \sum_{k=0}^{31} b_k 2^k\)), где је \(i\) текућа вредност променљиве i, док је \(n_0\) почетна, а \(n\) текућа вредност неозначеног броја n.

Доказ. Докажимо да је наведени услов инваријанта.

Теорема 1.A.4. По завршетку алгоритма низ садржи бинарни запис неозначеног броја n.

Доказ. Како је по изласку из петље \(n=0\), на основу инваријанте важи да је \(b = n_0\) тј. да низ садржи бинарни запис полазног броја. \(\Box\)

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

1.A.3 Хорова логика

Формална спецификација програма може се задати у облику Хорове тројке. У том случају предуслов описује услове који важе за улазне променљиве, док постуслов описује услове које би требало да задовоље резултати израчунавања. На пример, програм P за множење бројева \(x\) и \(y\), који резултат смешта у променљиву \(z\) би требало да задовољи тројку \(\{\top\}\)P\(\{z = x\cdot y\}\) (\(\top\) означава исказну константу тачно, и овом примеру значи да нема предуслова које вредности \(x\) и \(y\) треба да задовољавају). Ако се задовољимо тиме да програм може да множи само ненегативне бројеве, спецификација се може ослабити у \(\{x \geq 0\ \wedge\ y \geq 0\}\)P\(\{z = x\cdot y\}\).

Једно од кључних питања за верификацију је питање да ли је нека Хорова тројка тачна (тј. да ли програм задовољава дату спецификацију). Хор је дао формални систем (аксиоме и правила извођења) који омогућава да се тачност Хорових тројки докаже на формалан начин (слика @fig:horov_sistem). За сваку синтаксну конструкцију програмског језика који се разматра формирају се аксиоме и правила извођења који дају ригорозан опис семантике одговарајућег конструкта програмског језика.2

Опис аксиоме и правила Хорове логике:

Докази исправности програма у оквиру Хорове логике користе инстанце аксиома (аксиоме примењене на неке конкретне наредбе) и из њих, применом правила, изводе нове закључке. Докази се могу погодно приказати у виду стабла, у чијем су листовима примене аксиома.

Степеновање

Докажимо коректност алгоритма степеновања. Потребно је доказати следећу тројку.

\[ \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} \]

На основу правила доделе примењеног на доделе i:=0 и m:=0 и два пута примењеног правила композиције важи тројка

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

Довољно је, дакле, да докажемо тројку

\[ \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} \]

Применимо правило петље на ову петљу уз инваријанту \(\varphi \equiv x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\). Потребно је доказати да тело петље чува инваријанту тј. доказати тројку:

\[ \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} \]

тј. \[ \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} \]

Након прве доделе, на основу правила доделе, важи тројка

\[ \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} \]

Заиста, заменом променљиве \(m\) изразом \(m\cdot x\) у постуслову и скраћивањем вредности \(x\) (што је допуштено, јер важи \(x > 0\)) добија се тачно предуслов.

Након друге доделе, на основу правила доделе важи тројка

\[ \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} \]

Заиста, заменом вредности \(i\) са \(i+1\) у постуслову добија се услов \(x > 0 \wedge k \geq 0 \wedge 0 \leq i+1 \leq k \wedge m = x^{i+1}\), који је логичка последица предуслова. Дакле, комбиновањем правила последице и правила композиције добија се тројка која гарантује да тело петље задовољава инваријанту, одакле, на основу правила петље, следи тројка

\[ \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} \]

Постуслов имплицира \(i=k\), па зато и жељени услов \(m = x^k\). Остало је још да се претходна тројка споји са тројком

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

коју смо раније доказали. За то је довољно приметити да услов \(x > 0 \wedge k \geq 0 \wedge i = 0 \wedge m = 1\) повлачи услов инваријанте \(x > 0 \wedge k \geq 0 \wedge 0 \leq i \leq k \wedge m = x^i\). Зато се тројка која закључак правила петље, на основу правила последице, може заменити жељеном тројком:

\[ \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} \]

Сада на основу правила композиције следи коректност целог алгоритма тј. тројка:

\[ \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 Софтвер за доказивање коректности програма

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

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

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

// 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. Основна разлика између рачунарског вируса и рачунарског црва је у томе што вирус мора бити активиран некаквом акцијом на рачунару на којем се налази. С друге стране, црв је самостални програм који може да се реплицира и шири чим допре до неког рачунарског система.↩︎

  2. У свом оригиналном раду, Хор је разматрао веома једноставан програмски језик (који има само наредбу доделе, наредбу гранања, једну петљу и секвенцијалну композицију наредби), али у низу радова других аутора Хоров оригинални систем је проширен правилима за сложеније конструкте програмских језика (функције, показиваче, итд.).↩︎