Formal Specification

The specification of a system using a precise and unambiguous language like Z, VDM or CSP. Unambiguous specifications are inherently testable, and impossible to interpret in more than one way.

-- JasonGorman

What do you mean by testable? What are you testing it against?

And "Unambiguous specifications are [...] impossible to interpret in more than one way" is just a tautology. That's what unambiguous means, Shirley?

---

I don't like the previous definition, so I'll suggest my own:

Formal specification is the specification of a program's properties in a language defined by a mathematical logic. Strictly speaking, this specification need not be executable (and hence not testable), however most languages used to formally specify programs have an associated operational semantics to allow executing the specification and testing a program's properties.

Examples of some commonly used formal specification languages include:

• ZedLanguage
• VDM
• CSP

I haven't actually used any of the above so somebody else should comment.

• ACL2 http://www.cs.utexas.edu/users/moore/acl2/
• PVS http://pvs.csl.sri.com/
• Maude http://maude.cs.uiuc.edu/

Writing code in the preceding three is similar to writing code in a functional language (particularly ACL2 as the underlying logic of ACL2 is an extension to an applicative first-order subset of CommonLisp). Reasoning is based on rewriting where a term is rewritten into equivalent terms (e.g. a function call may be rewritten into its body). Theorems may be proven solely through rewriting or using induction.

More opinion:

It is fundamentally impossible for any formal specification to completely capture a system. Even if one were to model the semantics of the programming language, the compiler, the operating system, and all the hardware (processor, motherboard, network card, etc), it would still be possible for a cosmic ray to come along and change a memory bit. So formal specification and a TheoremProving will never show a given property to be absolutely true. In addition, for many projects the formal specification may not be any clearer than the program itself.

Formal specification can still be quite useful for some projects, because the techniques of ModelChecking? and TheoremProving can be used to give guarantees that are not possible via UnitTesting, and since the formal specification need not be directly executable, it may be possible to use a higher level of abstraction than a conventional programming language is capable of. What is an appropriate specification depends both on the system being specified and the properties of interest.

Perhaps what these guarantees are should be spelled out in appropriate pages.

See ProofOfCorrectness, ProofsCantProveTheAbsenceOfBugs, FormalModelChecking

Thank you for the links.

-- JoeHendrix

Please do write more. It's interesting and on topic.