The primary idea behind a formal method lies in the writing of a precise specification of a system, using, therefore, a formal syntax and semantics. Semantics give precise meaning to components.
A specification of a system might cover one or more of a number of aspects, including its functional behavior, its structure, or its architecture, but also nonfunctional aspects such as timing or performance.
A precise system specification can be used in a number of ways: for understanding the system and for transforming it, thereby revealing errors or incompleteness. The specification can also sometimes be animated (e.g., in VDM-SL) or properties can be verified using formal proofs.
A specification can also be used for driving the development process, either by refining the specification into code or by direct code generation (sometimes after a certain number of transformations). Of course, testing is an aspect of the development process, and a specification can also be used to support the testing process by providing test cases and oracles.
A variety of different formal specification techniques exist; some are general-purpose techniques and others stress aspects relevant to particular application domains, e.g., concurrent or real-time systems. Most have tool support (e.g., the IFAD VDM-SL Toolbox; see http://www.ifad.dk/). Next we'll examine the most notable categories of methods.
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.