algorithm - 2 つの日付間の時間の計算の正確さを証明する

Question

特定の時間単位で2つの日付間の時間を計算することになっている非常に単純な関数があり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 少しばかげた実装のように見えることは無視してください - それは重要ではありません。