Нека је низ од 32 логичке вредности попуњен вредношћу false. Бинарни запис одређујемо тако што одређујемо једну по једну бинарну цифру броја, здесна налево. У сваком кораку петље одређујемо остатак при дељењу броја \(n\) са \(2\), и на наредно место у низу (у кораку \(i\) на место \(i\)) уписујемо true ако је тај остатак једнак 1. На крају петље, исписујемо садржај низа уназад.
Пример. Прикажимо извршавање алгоритма на примеру превођења броја 38 у бинарни запис. Приказаћемо само кораке који се изводе док \(n\) не постане 0 (од тог тренутка надаље низ се само попуњава нулама).
n niz b 38 19 0 9 10 4 110 2 0110 1 00110 0 100110
Имплементација се може направити на следећи начин.
#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\).
Лема: Услов \(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.
Доказ:
Заиста на почетку је \(n = n_0\), \(i = 0\) и \(b = 0\) па тврђење важи.
Претпоставимо да тврђење важи при уласку у петљу. Променљиве се током извршавања тела и корака петље мењају на следећи начин. \(n' = n \,\mathrm{div}\,2\), \(b' = b + 2^i\cdot (n \,\mathrm{mod}\,2)\) и \(i' = i+1\). Тада је \(2^{i'} \cdot n' + b'\) = \(2^{i+1} \cdot (n \,\mathrm{div}\,2) + b + 2^i \cdot n \,\mathrm{mod}\,2\) = \(2^i\cdot(2\cdot (n \,\mathrm{div}\,2) + n \,\mathrm{mod}\,2) + b\). На основу дефиниције целобројног дељења важи да је \(2 \cdot (n \,\mathrm{div}\,2) + n \,\mathrm{mod}\,2 = n\), па је вредност претходног израза једнака \(2^i\cdot n + b\), а на основу претпоставке о томе да инваријанта важи на уласку у тело петље знамо да је то једнако \(n_0\).
Теорема: По завршетку алгоритма низ садржи бинарни запис неозначеног броја n.
Доказ: Како је по изласку из петље \(n=0\), на основу инваријанте важи да је \(b = n_0\) тј. да низ садржи бинарни запис полазног броја.
Заустављање је прилично очигледно јер је n ненегативан број који се у сваком кораку стриктно смањује (све док не достигне нулу).
Сложеност. У овом облику алгоритма се увек спровди 32 корака, па је сложеност константна. У општем случају можемо сматрати да је линеарна у односу на број цифара у бинарном запису (она логаритамски зависи од величине броја \(n\)).
U narednom apletu možete videti korake u izvršavanju ovog algoritma i uveriti se da u svakom koraku invarijanta važi.
✖