algorithm - 证明计算两个日期之间的时间量的正确性

Question

我有一个非常简单的函数，它应该以给定的时间单位计算两个日期之间的时间量，例如：getPartialPeriod(January 1, February 15, months)将导致1.5.

我真的很纠结如何证明它——我从循环开始，因为我认为这是最困难的部分。我定义了许多 Hoare 三元组和循环不变量，却发现它们都没有用。我会很感激我能得到的所有帮助。

函数伪代码：

getPartialPeriod(startDate, endDate, timeUnitType):
    partialPeriod = 0
    currentDate = startDate + 1 timeUnit

    CASE timeUnitType
        weeks:   daysInTimeUnit = 7
        months:  daysInTimeUnit = 30
        DEFAULT: daysInTimeUnit = 1
    END CASE

    WHILE currentDate <= endDate DO 
        INCREMENT partialPeriod
        currentDate = currentDate + timeUnit
    END WHILE

    remainingPeriod = amount of days between currentDate and endDate
    partialPeriod = partialPeriod + remainingPeriod / daysInTimeUnit

PS请忽略这似乎是一个愚蠢的实现 - 这并不重要。