Escher Technologies - Perfect Developer and SPARK Ada

Formal Software Specification Made Easier

The benefits of formal specification have long been recognized by the writers of ultra-reliable software. In the past, software specifications have often been written in Z, a language with a steep learning curve and limited tool support.

Now there is an alternative: the Perfect specification language, supported by the Perfect Developer tool.

Perfect for easy learning!

Perfect Developer - Making software bugs extinct!

The Perfect specification language builds on standard concepts from procedural, object-oriented, and functional programming languages, with mathematical notation kept to a minimum, using the principles of Verified Design by Contract.

This specification language is much easier than Z for most software developers to learn. Like Z, Perfect supports refinement of high-level to low-level specifications.

Perfect Developer for automatic proof!

The Perfect specification language is supported by the Perfect Developer tool, which includes a powerful automatic theorem prover for producing verification proofs without user intervention. This means you can easily and economically verify your specifications as you develop and refine them.

From specification to code

If you use MISRA-C, then Escher C Verifier will help you.

Perfect Developer can be paired with SPARK Ada, allowing high-level specifications to be refined to low-level specifications and carried through to SPARK-annotated Ada code. We provide support for partial SPARK Ada code generation, as well as full prototype code generation in a choice of other languages.

Interested?

If you would like some more information, please contact us .