I need to learn a notational language, so I can express and possibly prove the correctness of what I believe to be a complicated algorithm that distributes a credit adjustment across multiple water bills in issue date descending order. But I cannot tell what that notational language should be.

Each bill has three consumption tiers, 1-30, 31-60, and over 60. Each tier is associated with a different water and sewer rate. The higher the tier, the higher is the rate.

Two water bills each have 100ccf consumption, which means each bill is billed like this. That is it’s distribution across tiers 1, 2, and 3 is tier1 = -30, tier2 = -30, and tier3 = -40. In case it is not obvious, billing takes place from lowest to highest tier, so crediting takes place from highest to lowest tier.

If I apply a -170 consumption credit, the first bill consumes -100ccfs. It is the remaining -70 ccf credit to be applied to the second bill that gets crazy.

-40 of it has to be credited at tier3 and the remaining -30 at tier2. Nothing is left over for tier1 (second bill). I know this is absolutely correct distribution, because I’ve consulted the oracles in our municipality. They know what they’re talking about.

With -70 left (held in one variable) and the second bill’s original consumption (held in a separate variable), I subtract the value of the sum of tier1’s and tier2’s cutoffs (60ccf) from 100ccf (the consumption when the bill was issued). I want to prove why that is right. I’m not content to say “Hey, I fooled around until I got a nice answer.”

Any ideas or help would be appreciated.