Team. On Wednesday, we reviewed a few ideas on how contracts can raise the "odds" of ensuring the halt-ability of an application. A few more notes are necessary for justifying this since it counters the "well-accepted" notion set forth by Goedel. As stated on Wednesday, a program will eventually "halt" with a correct or incorrect result if all of its contracts are correct. These contracts are represented by conditional guards placed at various point in the application, and they will "gracefully" halt the program if the state of the internal data ever ventures outside of its allowed bounds. Given that each of the contracts has been written properly, the program must eventually halt if its design requires this. Since the contracts represent a very small subset of the total number of code lines, one can focus on the correctness of these as a starting point in ensuring the correctness of the program.
Furthermore, if we assume that the probability of error in any given instruction is q, then the odds that c contracts are correct is POWER( ( 1-q ) , c ) using the Excel function for exponentiation. This is the result of the hyper-geometric distribution which describes how one determines the odds of s sequential events with a probability of p occurring. This total probability is simply p with an exponent of s. Now realizing that the probability of the remaining lines of code all being correct is POWER( (1 - q), (n-c) ) where n is much greater than c, one can insure halt-ability with a greater probability thorough the use of contracts.We should also mention that q must be less than 1.
Contracts as a Concerns
Contracts are fundamental concerns of any system whether they are actually formally addressed during its development or not.
CABOOSE and Halt-ability
The CABOOSE source contains a few explicit and implicit contracts in the form of conditional guards which measure the state of key variables. If the state of any of the monitored variables exceeds a boundary, an exception is raised. Will CABOOSE always halt? This is a excellent question. Considering that our original goal was simplicity and the code-base is less than a 0.5 KLOC, one will likely remember the earlier quote placed in this weblog that stated:
One can develop software in such a manner that it does not have any obvious errors or that it obviously does not have any errors.
In other words, it can be so incredibly "confusing" and "complex" that one cannot find any mistakes in it. Or, it can be so simple and well-written that any coding flaws jump off the page.
Our goal with CABOOSE is that flaws leap out of NetBeans when we read the source. Unfortunately, they have not always done so.
Enjoy this weekend....
No comments:
Post a Comment