docs/manual/units-checker.tex

\htmlhr
\chapterAndLabel{Units Checker}{units-checker}

For many applications, it is important to use the correct units of
measurement for primitive types.  For example, NASA's Mars Climate Orbiter
(cost: \$327 million) was lost because of a discrepancy between use
of the metric unit Newtons and the imperial measure Pound-force.

The \emph{Units Checker} ensures consistent usage of units.
For example, consider the following code:

\begin{alltt}
@m int meters = 5 * UnitsTools.m;
@s int secs = 2 * UnitsTools.s;
@mPERs int speed = meters / secs;
\end{alltt}

Due to the annotations \<@m> and \<@s>, the variables \code{meters} and \code{secs} are guaranteed to contain
only values with meters and seconds as units of measurement.
The assignment of an unqualified value to \code{meters}, as in
\code{meters = 99}, will be flagged as an error by the Units Checker.
Utility class \refclass{checker/units/util}{UnitsTools} provides constants
that you can multiply with unqualified integer are multiplied to get values
of the corresponding unit; for example, \code{meters = 99 *
  UnitsTools.m} is legal, or just \code{meters = 99 *
  m} if the file contains
\<import static org.checkerframework.checker.units.util.UnitsTools.*;>.
To use the \refclass{checker/units/util}{UnitsTools} class, the
\<checker-util.jar> file must be on the classpath at run time.

The division \code{meters/secs} takes the types of the two operands
into account and determines that the result is of type
meters per second, signified by the \code{@mPERs} qualifier.
We provide an extensible framework to define the result of operations
on units.


\sectionAndLabel{Units annotations}{units-annotations}

The checker currently supports three varieties of units annotations:
kind annotations (\refqualclass{checker/units/qual}{Length},
\refqualclass{checker/units/qual}{Mass}, \dots),
the SI units (\refqualclass{checker/units/qual}{m}, \refqualclass{checker/units/qual}{kg}, \dots), and polymorphic annotations
(\refqualclass{checker/units/qual}{PolyUnit}).


Kind annotations can be used to declare what the expected unit of
measurement is, without fixing the particular unit used.
For example, one could write a method taking a \code{@Length} value,
without specifying whether it will take meters or kilometers.
The following kind annotations are defined:

\begin{description}
\item[\refqualclass{checker/units/qual}{Acceleration}]

\item[\refqualclass{checker/units/qual}{Angle}]

\item[\refqualclass{checker/units/qual}{Area}]

\item[\refqualclass{checker/units/qual}{Current}]

\item[\refqualclass{checker/units/qual}{Force}]

\item[\refqualclass{checker/units/qual}{Length}]

\item[\refqualclass{checker/units/qual}{Luminance}]

\item[\refqualclass{checker/units/qual}{Mass}]

\item[\refqualclass{checker/units/qual}{Speed}]

\item[\refqualclass{checker/units/qual}{Substance}]

\item[\refqualclass{checker/units/qual}{Temperature}]

\item[\refqualclass{checker/units/qual}{Time}]

\item[\refqualclass{checker/units/qual}{Volume}]
\end{description}

% \medskip


For each kind of unit, the corresponding SI unit of
measurement is defined:

\begin{enumerate}
\item For \code{@Acceleration}:
  Meter Per Second Square \refqualclass{checker/units/qual}{mPERs2}

\item For \code{@Angle}:
  Radians \refqualclass{checker/units/qual}{radians},
  and the derived unit
  Degrees \refqualclass{checker/units/qual}{degrees}

\item For \code{@Area}:
  the derived units
  square millimeters \refqualclass{checker/units/qual}{mm2},
  square meters \refqualclass{checker/units/qual}{m2}, and
  square kilometers \refqualclass{checker/units/qual}{km2}

\item For \code{@Current}:
  Ampere \refqualclass{checker/units/qual}{A}

\item For \code{@Force}:
  Newton \refqualclass{checker/units/qual}{N}
  and the derived unit
  kilonewton \refqualclass{checker/units/qual}{kN}

\item For \code{@Length}:
  Meters \refqualclass{checker/units/qual}{m}
  and the derived units
  millimeters \refqualclass{checker/units/qual}{mm} and
  kilometers \refqualclass{checker/units/qual}{km}

\item For \code{@Luminance}:
  Candela \refqualclass{checker/units/qual}{cd}

\item For \code{@Mass}:
  kilograms \refqualclass{checker/units/qual}{kg}
  and the derived units
  grams \refqualclass{checker/units/qual}{g} and
  metric tons \refqualclass{checker/units/qual}{t}

\item For \code{@Speed}:
  meters per second \refqualclass{checker/units/qual}{mPERs} and
  kilometers per hour \refqualclass{checker/units/qual}{kmPERh}

\item For \code{@Substance}:
  Mole \refqualclass{checker/units/qual}{mol}

\item For \code{@Temperature}:
  Kelvin \refqualclass{checker/units/qual}{K}
  and the derived unit
  Celsius \refqualclass{checker/units/qual}{C}

\item For \code{@Time}:
  seconds \refqualclass{checker/units/qual}{s}
  and the derived units
  minutes \refqualclass{checker/units/qual}{min} and
  hours \refqualclass{checker/units/qual}{h}

\item For \code{@Volume}:
  the derived units
  cubic millimeters \refqualclass{checker/units/qual}{mm3},
  cubic meters \refqualclass{checker/units/qual}{m3}, and
  cubic kilometers \refqualclass{checker/units/qual}{km3}
\end{enumerate}


You may specify SI unit prefixes, using enumeration \code{\refclass{checker/units/qual}{Prefix}}.
The basic SI units
(\code{@s}, \code{@m}, \code{@g}, \code{@A}, \code{@K},
 \code{@mol}, \code{@cd})
take an optional \code{Prefix} enum as argument.
For example, to use nanoseconds as unit, you could use
\code{@s(Prefix.nano)} as a unit type.
You can sometimes use a different annotation instead of a prefix;
for example, \<@mm> is equivalent to \<@m(Prefix.milli)>.

Class \code{UnitsTools} contains a constant for each SI unit.
To create a value of the particular unit, multiply an unqualified
value with one of these constants.
By using static imports, this allows very natural notation; for
example, after statically importing \code{UnitsTools.m},
the expression \code{5 * m} represents five meters.
As all these unit constants are public, static, and final with value
one, the compiler will optimize away these multiplications.
To use the \refclass{checker/units/util}{UnitsTools} class, the
\<checker-util.jar> file must be on the classpath at run time.

The polymorphic annotation \refqualclass{checker/units/qual}{PolyUnit}
enables you to write a method that takes an argument of any unit type and
returns a result of that same type.  For more about polymorphic qualifiers,
see Section~\ref{method-qualifier-polymorphism}.  For an example of its use, see
the
\href{../api/org/checkerframework/checker/units/qual/PolyUnit.html}{\<@PolyUnit>
Javadoc}.


\sectionAndLabel{Extending the Units Checker}{extending-units}

You can create new kind annotations and unit annotations that are specific
to the particular needs of your project.  An easy way to do this is by
copying and adapting an existing annotation.  (In addition, search for all
uses of the annotation's name throughout the Units Checker implementation,
to find other code to adapt; read on for details.)

Here is an example of a new unit annotation.

\begin{alltt}
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(\{ElementType.TYPE_USE, ElementType.TYPE_PARAMETER\})
@SubtypeOf(\ttlcb{}Time.class\ttrcb{})
@UnitsMultiple(quantity=s.class, prefix=Prefix.nano)
public @interface ns \ttlcb{}\ttrcb{}
\end{alltt}

The \code{@SubtypeOf} meta-annotation specifies that this annotation
introduces an additional unit of time.
The \code{@UnitsMultiple} meta-annotation specifies that this annotation
should be a nano multiple of the basic unit \code{@s}:  \code{@ns} and
\code{@s(Prefix.nano)}
behave equivalently and interchangeably.
Most annotation definitions do not have a \<@UnitsMultiple> meta-annotation.

Note that all custom annotations must have the
\<@Target(ElementType.TYPE\_USE)> meta-annotation. See section
\ref{creating-define-type-qualifiers}.

To take full advantage of the additional unit qualifier, you need to
do two additional steps.
(1)~Provide constants that convert from unqualified types to types that use
the new unit.
See class \code{UnitsTools} for examples (you will need to suppress a
checker warning in just those few locations).
(2)~Put the new unit in relation to existing units.
Provide an
implementation of the \code{UnitsRelations} interface as a
meta-annotation to one of the units.

See demonstration \code{docs/examples/units-extension/} for an example
extension that defines Hertz (hz) as scalar per second, and defines an
implementation of \code{UnitsRelations} to enforce it.



\sectionAndLabel{What the Units Checker checks}{units-checks}

The Units Checker ensures that unrelated types are not mixed.

All types with a particular unit annotation are
disjoint from all unannotated types, from all types with a different unit
annotation, and from all types with the same unit annotation but a
different prefix.

Subtyping between the units and the unit kinds is taken into account,
as is the \code{@UnitsMultiple} meta-annotation.

Multiplying a scalar with a unit type results in the same unit type.

The division of a unit type by the same unit type
results in the unqualified type.

Multiplying or dividing different unit types, for which no unit
relation is known to the system, will result in a \code{MixedUnits}
type, which is separate from all other units.
If you encounter a \code{MixedUnits} annotation in an error message,
ensure that your operations are performed on correct units or refine
your \code{UnitsRelations} implementation.

The Units Checker does \emph{not} change units based on multiplication; for
example, if variable \<mass> has the type \<@kg double>, then \<mass *
1000> has that same type rather than the type \<@g double>.  (The Units
Checker has no way of knowing whether you intended a conversion, or you
were computing the mass of 1000 items.  You need to make all conversions
explicit in your code, and it's good style to minimize the number of
conversions.)


\sectionAndLabel{Running the Units Checker}{units-running}

The Units Checker can be invoked by running the following commands.

\begin{itemize}
\item
If your code uses only the SI units that are provided by the
framework, simply invoke the checker:

\begin{Verbatim}
  javac -processor org.checkerframework.checker.units.UnitsChecker MyFile.java ...
\end{Verbatim}

\item
If you define your own units, provide the fully-qualified class names of the
annotations through the \code{-Aunits} option, using a comma-no-space-separated
notation:

\begin{alltt}
  javac -classpath \textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} \ttbs
        -processor org.checkerframework.checker.units.UnitsChecker \ttbs
        -Aunits=\textit{myPackage.qual.MyUnit},\textit{myPackage.qual.MyOtherUnit} MyFile.java ...
\end{alltt}

The annotations listed in \code{-Aunits} must be accessible to
the compiler during compilation.  Before you run the Units Checker with
\code{javac}, they must be compiled and on the same path (the classpath or
processorpath) as the Checker Framework.  It
is not sufficient to supply their source files on the command line.

\item
You can also provide the fully-qualified paths to a set of directories
that contain units qualifiers through the \code{-AunitsDirs} option,
using a colon-no-space-separated notation. For example,
if the Checker Framework is on the classpath rather than the processorpath:

\begin{alltt}
  javac -classpath \textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} \ttbs
        -processor org.checkerframework.checker.units.UnitsChecker \ttbs
        -AunitsDirs=\textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} MyFile.java ...
\end{alltt}

Note that in these two examples, the compiled class file of the
\<myPackage.qual.MyUnit> and \<myPackage.qual.MyOtherUnit> annotations
must exist in either the \<myProject/bin> directory or the
\<myLibrary/bin> directory. The following placement of the class files
will work with the above commands:

\begin{alltt}
  .../myProject/bin/myPackage/qual/MyUnit.class
  .../myProject/bin/myPackage/qual/MyOtherUnit.class
\end{alltt}

The two options can be used at the same time to provide groups of annotations
from directories, and individually named annotations.

\end{itemize}

Also, see the example project in the \<docs/examples/units-extension> directory.



\sectionAndLabel{Suppressing warnings}{units-suppressing}

One example of when you need to suppress warnings is when you
initialize a variable with a unit type by a literal value.
To remove this warning message, it is best to introduce a
constant that represents the unit and to
add a \code{@SuppressWarnings}
annotation to that constant.
For examples, see class \code{UnitsTools}.


\sectionAndLabel{References}{units-references}

\begin{itemize}
\item The GNU Units tool provides a comprehensive list of units:\\
  \url{http://www.gnu.org/software/units/}

\item The F\# units of measurement system inspired some of our syntax:\\
  \url{https://en.wikibooks.org/wiki/F_Sharp_Programming/Units_of_Measure}

\end{itemize}

% LocalWords:  UnitsTools toMeter toSecond mPERs Candela cd kmPERh mol nano ns
% LocalWords:  milli RetentionPolicy SubtypeOf UnitsMultiple hz PolyUnit
% LocalWords:  UnitsRelations Aunits MyFile mm2 m2 km2 enum ElementType
%  LocalWords:  MixedUnits java mPERs2 api classpath bootclasspath RUNTIME
%%  LocalWords:  AunitsDirs myProject myLibrary Luminance processorpath