 The latter is a full-fledged specification, though expressed in a natural language. Specifications are often advanced in a natural language to be closer to the stakeaholder’s intentions and only subsequently they are formalized in a proper formal language. Specifications may be expressed by means of graphical languages such as UML (Fowler 2003), or more formal languages such as TPL (Turner 2009a) and VDM (Jones 1990), using predicate logic, or Z (Woodcock and Davies 1996), focusing on set theory. For instance, Type Predicate Logic (TPL) expresses the requirements of computational systems using predicate logic formulas, wherein the type of the quantified variables is specified. The choice of the variable types allows one to define specifications at the more appropriate abstraction level. Whether specifications are expressed in an informal or formal guise often depends on the development method followed, with formal specifications usually preferred in the context of formal development methods. Moreover, formal specifications facilitate verification of correctness for computational systems (see  §6).