Одређивање записа броја n0 у основи b

Алгоритам:

        n = n0;
        digits = [];
        while (n > 0) {
           digits.push_back(n % b);
           n = n / b;
        }
      

Спровођење алгоритма корак по корак:

Прикажи инваријанту: