Well-measuring programs

Any program that measures quantities from its physical environment must compute using correct and consistent units of measurement. Such a program is described as well-measuring. In many systems, particularly embedded control software, paying inadequate attention to units of measurement can result in catastrophe. Unfortunately, current programming languages and tools provide little aid to the programmer attempting to establish or verify the well-measuring property. We present a program analysis technique for inferring and checking the units used within a program. The technique combines traditional Hindley-Milner-style type inference with the use of static single assignment (SSA) form to enable analysis of imperative programs.