Using units of measurement in formal specifications

In the physical sciences and engineering, units of measurement provide a valuable aid to both the exposition and comprehension of physical systems. In addition, they provide an error checking facility comparable to static type checking commonly found with programming languages. It is argued that units of measurement can provide similar benefits in the specification and design of software and computer systems.To demonstrate this, we present an extension of the Z specification notation with support for the incorporation of units in specifications and demonstrate the feasibility of static dimensional analysis of the resulting language.