The technology behind Perfect Developer: Object-Oriented Formal Methods

It has long been realised that the behaviour of software components and even complete software and hardware systems can be described using mathematics. Similarly, the meaning of program language statements can be defined mathematically. In principle, the meanings of individual statements can be combined to calculate the meaning of a complete program, which can then be compared with a mathematical description of the required behaviour.

The use of mathematics to define and verify the behaviour of software is called formal methods. Aerospace companies and other writers of safety-critical software have long used formal methods to help ensure that their software is dependable.

Unfortunately, it has not been economic to apply formal methods to the development of non-critical software. The tools available were generally not object-oriented and required the developer to express specifications using unfamiliar mathematical notations and to assist in the theorem-proving process. Further, the semantics of the specification language were often far removed from the semantics of the programming languages used to write code, making it harder to relate the two.

Perfect Developer uses a single easy-to-learn language to describe both specifications and program statements. Making use of recent advances in automated reasoning technology, Perfect Developer includes a fully automatic theorem prover so that the user does not need extensive mathematical knowledge.

Taken with Perfect Developer's ability to generate code automatically from simple specifications and its high-level data types, these features finally make the development of highly reliable software possible without sacrificing developer productivity.

More information on formal methods can be found here.