Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software.

They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools.

A good specification must have some of the following attributes: adequate, internally consistent, unambiguous, complete, satisfied, minimal.

[4] This may be for a variety of reasons, some of which are: Other limitations:[3] Formal specification techniques have existed in various domains and on various scales for quite some time.

[6] Implementations of formal specifications will differ depending on what kind of system they are attempting to model, how they are applied and at what point in the software life cycle they have been introduced.

Others include the Specification Language (VDM-SL) of the Vienna Development Method and the Abstract Machine Notation (AMN) of the B-Method.