У овом поступку се комбинују два алгоритма. Први је алгоритам за одређивања цифара у декадном запису броја, здесна налево, одређивањем остатка при целобројном дељењу. Други алгоритам је Хорнерова схема за одређивање вредности броја на основу његових цифара слева надесно. Тај алгоритам је описан у задатку Број формиран од датих цифра с лева на десно. Скидамо једну по једну цифру броја \(n\) здесна и дописујемо је на резултат, такође здесна.
Пример. Размотримо поступно рад алгоритма на једном примеру.
n r i 123000 0 0 12300 0 1 1230 0 2 123 0 3 12 3 4 1 32 5 0 321 6
Коректност овог алгоритма се заснива на следећој инваријанти. Након \(i\) корака петље број \(n\) садржи број који се добије када се од почетног броја \(n_0\) обрише последњих \(i\) цифара, док број \(r\) садржи број који се добије обртањем тих последњих \(i\) цифара броја \(n_0\).
Имплементација се може направити на следећи начин.
#include <iostream>
using namespace std;
int obrni(int n) {
int r = 0;
while (n > 0) {
r = 10*r + n % 10;
n /= 10;
}
return r;
}
int main() {
int n;
cin >> n;
cout << obrni(n) << endl;
return 0;
}Доказ коректности. Пошто је програм написан у терминима математичких операција, ако желимо да спроведемо потпуно прецизан, математички формалан доказ, и инваријанту морамо изразити у терминима математичких операција. Нажалост, испоставиће се да крајње нуле у запису броја, које постају водеће нуле у резултату значајно компликују прецизно изражавање инваријанте и наставак доказа чине прилично мукотрпним. Наиме, број који се обрће може се завршити нулама, тако да на пример бројеви \(123\), \(1230\), \(12300\) сви имају исту вредност броја који се записује истим цифрама као оригинални број али у обрнутом поретку (\(321\)). Али број корака петље који ће бити потребан да се та вредност израчуна ће се разликовати у тим ситуацијама (и биће једнак броју цифара броја \(n\)). Отуда је битно приметити да је број завршних нула у запису броја битан за предложени алгоритам.
Лема: Услов да је \(n_0 = n \cdot 10^i + \mathit{rev}(r) \cdot 10^s\) (где је \(s\) број завршних нула у запису броја \(n_0\)) је инваријанта петље. При том је број \(r\) једнак 0 док је \(i \leq s\) (има 0 цифара у запису), односно има тачно \(i-s\) цифара у запису када је \(i > s\) и водећа цифра му је различита од нуле. Важи и да је \(n \geq 0\).
Докажимо ову лему.
Пре првог уласка у петљу је \(n = n_0\), \(r = 0\) и \(i = 0\), па услов очигледно важи.
Претпоставимо да тврђење важи на уласку у петљу. Ефекат тела петље је да је \(n' = n \,\mathrm{div}\,10\), да је \(r' = 10r + n \,\mathrm{mod}\,10\) и да је \(i' = i + 1\). Потребно је да докажемо да вредност \(n' \cdot 10^{i'} + \mathit{rev}(r') \cdot 10^s\) остаје једнака \(n_0\). Након извршавања тела петље, она је једнака \((n \,\mathrm{div}\,10) \cdot 10^{i+1} + \mathit{rev}(10r + n \,\mathrm{mod}\,10) \cdot 10^s\). Ову вредност даље израчунавамо у зависности од односа променљивих \(i\) и \(s\).
Ако је \(i < s\), петља скида нуле са краја записа броја \(n\), тада је \(r = 0\) и \(n \,\mathrm{mod}\,10 = 0\). Зато је претходна вредност једнака \((n \,\mathrm{div}\,10) \cdot 10^{i+1} = (10\cdot (n \,\mathrm{div}\,10) + n \,\mathrm{mod}\,10)\cdot 10^i = n\cdot 10^i\), што је на основу претпоставке једнако \(n_0\) (јер је и у претходном кораку \(r = 0\)).
Ако је \(i = s\) петља је стигла до прве цифре различите од нуле, па је још увек \(r=0\), а \(n \,\mathrm{mod}\,10 \neq 0\). Пошто је \(n \,\mathrm{mod}\,10\) једноцифрен број, важи да је \(\mathit{rev}(n \,\mathrm{mod}\,10) = n \,\mathrm{mod}\,10\). Пошто је \(i = s\), вредност израза који фигурише у инваријанти једнака је \((n \,\mathrm{div}\,10) \cdot 10^{i+1} + (n \,\mathrm{mod}\,10) \cdot 10^i = (10\cdot (n \,\mathrm{div}\,10) + n \,\mathrm{mod}\,10) \cdot 10^i = n \cdot 10^i\), а то је на основу претпоставке једнако \(n_0\) (јер је и у претходном кораку \(r = 0\)). Важи и да је \(r' = n \,\mathrm{mod}\,10\), па је \(0 < r' < 10\) и \(r'\) је једноцифрен број. Зато важи да \(r'\) има тачно \(i' - s = i + 1 - i = 1\) цифара и да му је водећа цифра различита од нуле.
Ако је \(i > s\), пошто \(r\) има тачно \(i - s\) цифара, тада важи да је \(\mathit{rev}(10r + n \,\mathrm{mod}\,10) = (n \,\mathrm{mod}\,10)\cdot 10^{i-s} + \mathit{rev}(r)\). Заиста, израз са леве стране означава број који се добија обртањем редоследа цифара броја који се од броја \(r\) добија дописивањем цифре \(n \,\mathrm{mod}\,10\) (она може бити и нула) с десне стране. Што се тиче израза са десне стране, на основу инваријанте знамо да је \(r\) број који има тачно \(i - s\) цифара и оне одговарају степенима од \(10^0\) до \(10^{i-s-1}\). Зато се цифра \(n \,\mathrm{mod}\,10\) множењем са фактором \(10^{i-s}\) поставља као прва цифра иза које следе све цифре записа броја \(r\) у обрнутом редоследу. Дакле, леви и десни израз имају исту вредност. На основу тога, знамо да је вредност израза који фигурише у инваријанти након извршавања тела једнака \(n' \cdot 10^{i'} + \mathit{rev}(r') \cdot 10^s\) = \((n \,\mathrm{div}\,10)\cdot 10^{i+1} + \mathit{rev}(10r + n \,\mathrm{mod}\,10)\cdot 10^s\) = \((n \,\mathrm{div}\,10) \cdot 10^{i+1} + ((n \,\mathrm{mod}\,10) \cdot 10^{i-s} + \mathit{rev}(r)) \cdot 10^s\) = \((10\cdot(n \,\mathrm{div}\,10) + n \,\mathrm{mod}\,10)\cdot 10^i + \mathit{rev}(r)\cdot 10^s\) = \(n\cdot 10^i + \mathit{rev}(r)\cdot 10^s\), што је једнако \(n_0\) на основу претпоставке. Пошто је \(r' = 10r + n \,\mathrm{mod}\,10\), онда важи да \(r'\) има једну цифру више него \(r\) (тј. има \(i - s + 1 = i' - s\) цифара), а водећа цифра је различита од нуле (водећа цифра се није променила).
Теорема: Након извршавања кода важи да је \(r = \mathit{rev}(n_0)\).
Пошто је \(n \geq 0\) и није \(n > 0\) (јер се петља завршила), важи да је \(n = 0\). Зато је \(n_0 = \mathit{rev}(r) \cdot 10^s\). тј. \(\mathit{rev}(r) = \frac{n_0}{10^s}\). Пошто је водећа цифра броја \(r\) различита од нуле и пошто је последња цифра броја \(\frac{n_0}{10^s}\) такође различита од нуле (јер \(n_0\) има тачно \(s\) завршних нула које се дељењем са \(10^s\) бришу), важи да је \(r = \mathit{rev}(\frac{n_0}{10^s})\). Међутим, важи и да је \(\mathit{rev}(n_0) = \mathit{rev}(\frac{n_0}{10^s})\), јер \(\mathit{rev}(n_0)\) има тачно \(s\) водећих нула које се могу обрисати без утицаја на коначни резултат.
Заустављање се доказује прилично једноставно јер је \(n \geq 0\) и константно се смањује, па мора доћи до нуле.