This section contains 253 words (approx. 1 page at 300 words per page) |
An assertion is a statement about a part of a program that is either true or false. Two types of assertions, invariant and variant, function in the verification process of programming. Verification consists of proving logically that the programming sequence will lead to the desired objective, no matter what the data are, or how many programming steps are necessary.
The verification process involves a mathematical property called induction. Induction asserts, or assumes to be true, that the state after each programming step is suitable for the start of the next step. The assertion that the state remains suitable from step to step is the invariant assertion. Maintaining suitable states does not guarantee the satisfactory achieving of the programming objective. It must also be demonstrated that each programming step incrementally advances towards the object, and that only a finite number of increments are possible. Otherwise, a program could run indefinitely without giving an answer.
In contrast to an invariant assertion, a variant assertion is a statement that can start out as true or false but will be changed to the opposite value by the time the programming sequence ends. A variant assertion is more complex than an invariant assertion, and deals with the programming logic that ensures that a programming sequence will eventually end. The variant statement is typically used when the sequence of commands does not repeat, or iterate.
Usually the true form of an assertion, whether invariant or variant, is used in programming verification.
This section contains 253 words (approx. 1 page at 300 words per page) |