2

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.

octopusgrabbus
  • 699
  • 1
  • 8
  • 20
  • Why exactly lambda calculus? LC is primarily theoretical construct, it is not good to use for implementation of specific algorithms. Unless you mean functional code in general? – Euphoric Aug 01 '14 at 21:44
  • Doesn't have to be LC. I'm looking for a meta language to express and then prove the algorithm. I've edited the OP to ask a more general question and leave LC out. Add wording for proving correctness. – octopusgrabbus Aug 01 '14 at 21:44
  • You should then say it more explicitly that you are looking for a proof of correctness of your algorithm too. – Euphoric Aug 01 '14 at 21:46
  • Edited OP per this comment. – octopusgrabbus Aug 01 '14 at 21:49
  • Take a look at [Coq](http://coq.inria.fr). It's an amazingly powerful language and proof system, and can extract to efficient OCaml code. – Lily Chung Aug 01 '14 at 21:51
  • 2
    Maybe you should try asking http://cs.stackexchange.com/ . They are probably much more experienced with formal proof of algorithms than here. And let me warn you : Formal proofs are extremely complex subject. The way you are asking, it seems you have a lot to learn. – Euphoric Aug 01 '14 at 21:52
  • 1
    Completely disregarding the meta language, I'd approach this in a slightly TDD way. You've got some excellent expected input/output states there which could be codified into tests that would serve as some runnable documentation – Daenyth Aug 01 '14 at 21:57

1 Answers1

2

As I expressed in another answer, Z-Notation is a common standard method in formal CS for expressing algorithms independent of programming language. The broader category is Pidgin Code.

Z-Notation is used in both Introduction to Algorithms and Artificial Intelligence: A Modern Approach, both standard textbooks in their respective sub-disciplines and containing some very complex examples rendered beautifully in Z-Notation.

You can, of course, use whatever notation you desire but since Z-Notation is widely used and developed by researchers working in theoretical Computer Science and Mathematics, it will allow a wider audience than many of the alternatives.

Community
  • 1
  • Thanks. I'll go look for this. I can express my algorithm using common sense. I know why it works, but not from a more formal standpoint. – octopusgrabbus Aug 01 '14 at 23:57