阶乘数系统算法的形式证明

Question

我想出了一个算法，用于在阶乘数字系统中找到给定数字的表示。我很难以正式的方式证明它的正确性。这是Python中的代码（注意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

实际上很难“证明”一个包含“打印”语句的程序。您最好将这些值附加到列表中，然后打印或返回该列表。你有一些可以反对的理由。所以让我们假设你在某个地方有result = []，而你的“out +=”语句是result.append(n//s)

所以。你有两个循环，你需要两个循环不变量。首先，您需要显示s = k!。对于第二个循环，您需要证明带有k 零的result 是the_value_of_n_passed_as_an_argument_to_the_function - n 的阶乘表示。这两者都应该相对简单。最后，你得到了k == 0，这意味着result 是n 的原始值的阶乘表示。