Finally let's consider the termination problem: We shall prove that every loop terminates eventually. For this aim, a positive expression, that is one strictly decreasing at every loop iteration and reaching 0 at the loop's end, must be exhibited. This monotonic decreasing expression guarantees that termination eventually occurs. You can often guess it from the loop invariant. For instance, a termination expression of the outer loop L of the bubble sort example is

It is obvious that Term_L starts with the value MAX_ITER, ends with 0, and is always positive.

This C verification method relies on the production of a pre- and post-condition for every function and a proof of correctness of each such annotated function. These two steps can, however, be decoupled, and it is perfectly acceptable to produce only specifications and leave the proofs for a later stage, especially when efforts are limited. The proof of the verification conditions is very time consuming and requires some mathematical background, essentially in algebra. On some numerical code, the complete specification and proof was estimated by the authors as consuming an effort equivalent to programming the application itself.8

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook

Post a comment