First Approach

Ideally, the Hoare method, from which the VDM method is derived, should be applied during the early stages of the development process. At a specification level, this means that the system's functions should be specified formally using VDM-SL and refined progressively. Refinements do not need to be formal refinements (such as in B) where each refinement (i.e., set of modules) is checked for conformance with regard to the original module. Several methods and support languages exist such as B or VDM. They provide a specification language that covers the global and detailed specification, the design and implementation phases by means of one language. This language allows us to describe the pre- and post-conditions as done previously, but also the pseudo-code of the functions. Object-orientation is often supported.

The specification of each code function initially consists of the signature of that function together with its pre- and post-conditions along with some possible code. A developer must, therefore, start writing some high-level functions and their specifications. Refinements consist in decomposing these functions into smaller and more manageable ones. Refinements, therefore, introduce new functions and modules to build up new functionalities that can be grouped into modules. Refinements also introduce new data types and/or refine existing ones. Global variables can also be grouped into a state vector. For instance, the signature of a function to compute the volume of a circular cone in VDM-SL can be written

CircConeVol : CirCone -> real

CircConeVol(c) == MATH'ExtPI * c.diameter * c.diameter * c.height/12.C Pre CircConeVol: c.diameter > C A c.height > C

The result of successive refinements is a set of functions that all have pseudo-code without any implicit construct (namely because these latter cannot be computed algorithmically and efficiently) and grouped into modules. Programming language code can be generated automatically and then compiled in turn. For instance, VDM-SL produces C/C++ code and B produces Ada code. This high-level code-generation phase guarantees that the target code respects the specification, but may not be optimal. In the latter case, the developer can optimize the target code by hand until it becomes satisfactory. Of course, a different path could be chosen, namely doing the code generation by hand or using a translator if some other target language is desired.

During the refinement process, functions must be checked for conformance with regards to their pseudo-code, as just described, by generating verification conditions and proving them. This proof phase is not mandatory but can increase confidence in the code in terms of reliability. Half of the proof phase, namely generating the verification conditions and performing their proof by hand, is also valuable.

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