Programming(Design) By Contract | Halt-ability

Team. This is short a note on contracts. For those of you unfamiliar with the concept of "programming by contract", we have included the following links which you can skim:
https://www.eiffel.com/values/design-by-contract/
http://en.wikipedia.org/wiki/Design_by_contract

This is very powerful technique. Consider, Goedel’s Halting Problem which argues that testing halt-ability is impossible. In other words, one cannot determine if a computer program which he has written will halt after it has started. Halt-ability is a fundamental question a programmer asks when he is checking the "correctness" of a program. Halt-ability does not guarantee "correctness", but is a pre-requirement for this in many cases.

Programming-by-contract can guarantee "halt-ability" of a program given that the source's contracts, a small subset of the instructions, are "correct". One achieves this goal by placing a contract in the form of a guard in front of important blocks of code. This guard is a conditional statement which checks the state of the programs key variables and ensures that they are in the appropriate ranges.

Given that the program receives correct input and each of the instructions of the program modifies this data correctly, the state of the program should have measurable bounds. If the data ever wanders outside these bound, one knows that the input was incorrect and the program might not halt on it. If the input was correct and its data reaches an out of bounds state, one can be certain that an error exists in the instructions, and the program might not halt. In either case, one can gracefully exit the program with an error digest. In which case, the program halts. Obviously, using contracts in the form of guards for ensuring halt-ability does not guarantee correctness since an "incorrect" instruction might modify data in such a way that it is not outside its value bounds but still is in error.

Contracts are a very powerful concept in computing and are not yet a buzzword among many professionals. One can represent the notion of a contract with many different computing structures besides conditionals. Abstractly put, a contract is an agreement between one region of a system and another. These contracts between the producer and the consumer of data can be explicitly or implicitly enforced. In fact, the requirement of javac that JAVA interfaces be fully defined represents the explicit enforcement of the contract between interface implementers and users.

Also, contracts are a rule used when programming and should be considered in design, but are not used in controlling the flow or accuracy of the design. So, design-by-contract would be more correctly called contractual design such as object-oriented design.

Zohar Manna wrote a wonderful text on program correctness in 1978 which is foundational for many of these concepts. Finding a copy is difficult, but it would be a great addition for any personal computing library.

Just a few notes. We should be working on the CABOOSE source this Saturday. Have a Great Day.