based on transitions from state-to-state of the system best used with a reactive system languages such as Statecharts, PROMELA, STeP-SPL, RSML or SCR rely on this paradigm Functional specification specify a system as a structure of mathematical functions OBJ, ASL, PLUSS, LARCH, HOL or PVS rely on this paradigm Operational Specification early languages such as Paisley, GIST, Petri nets or process algebras rely on this paradigm In addition to the above paradigms, there are ways to apply certain heuristics to help improve the creation of these specifications. The paper referenced here best discusses heuristics to use when designing a specification. They do so by applying a divide-and-conquer approach. Software tools The Z notation is an example of a leading formal specification language. Others include the Specification Language (VDM-SL) of the Vienna Development Method and the Abstract Machine Notation (AMN) of the B-Method. In the Web services area, formal specification is often used to describe non-functional properties (Web services quality of service). Some tools are: Algebraic Larch OBJ Lotos Model-based Z B VDM CSP Petri Nets TLA+ See also Algebraic specification Formal methods Model-based specification Software engineering Specification language Specification (technical standard) References External links A Case for Formal Specification (Technology) by Coryoth 2005-07-30 Formal methods Formal specification