This chapter provides an overview of how to determine if some Linux C code is reliable. The techniques used are based on formal methods whose application to real programs requires much effort and time but dramatically reduces the effort devoted to code testing. Details of the Hoare Logics and WP calculus were given and also instructions on how to apply them to C code. Many techniques and tools supporting Hoare Logics exist nowadays but no unified specification language exists for imperative languages, including C. The VDM specification and design method is of moderate complexity and can be learned quickly. It can be applied with different degrees of precision to analyze programs statically: It is already worthwhile to produce a VDM specification, turn it into an executable form, and evaluate it to find errors. For increased reliability, you can then generate verification conditions and also prove them using one or several provers.
The Hoare method requires more user intervention but allows you to specify C programs in much more detail and precision. The more recent abstract interpretation (AI) method requires less user presence but produces lower-level specifications and errors automatically. AI is a complement to Hoare Logics-based tools as it allows you to generate properties automatically (e.g., simple invariants) and use them during the intermediate predicates generation process.
This page intentionally left blank
Was this article helpful?
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.