Formal proof for a factorial number system algorithm

Question

I came up with an algorithm for finding the representation of a given number in the factorial number system. I have trouble proving its correctness in a formal way. Here is the code in Python (note that k! = s):

def fns(n):
    s = 1
    k = 1
    while s * (k + 1) <= n:
        k = k + 1
        s = s * k
    while k >= 1:
        print(n // s, end = "")
        n = n % s
        s = s // k
        k = k - 1

Answer 1

It's actually sort of hard to "prove" a program that has a "print" statement in it. You're better off appending the values to a list, and then printing or returning the list so that. you have something that can reason against. So let's assume that you somewhere have result = [], and your "out += " statement is instead result.append(n//s)

So. You have two loops, and you'll need two loop invariants. For the first look, you'll need to show that s = k!. For the second loop, you'll need to show that result with k zeros appended to it is the factorial representation of the_value_of_n_passed_as_an_argument_to_the_function - n. Both of these should be relatively straightfoward. At the end, you have that k == 0, so that means that result is the factorial representation of the original value of n.