Gimpel Software Blog Dimensional Analysis

Back in 1998, the $327.6 million project Mars Climate Orbiter built by NASA's Jet Propulsion Laboratory approached the Red Planet at the wrong angle resulting in the spacecraft's demise.What went wrong? It was discovered that different parts of the engineering team were using different units of measurement. One group working on the thrusters measured in English units of pounds-force seconds; the other used metric Newton-seconds.What can static analysis offer to help detect this type of issue? PC-lint/FlexeLint provides a (possibly underutilized) feature called Dimensional Analysis to prevent exactly these kinds of problems. Let's look at a small example.Dimensional Analysis Example// This example demonstrates dimensional analysis// FlexeLint will report whenever a variable (such as v)// that is typed as a Velocity is assigned anything other// than a Velocity or a Met/Sec//lint -e838 Suppress "Previously assigned value not used"//lint -strong( AcJcX, Met, Sec, Velocity = Met/Sec )typedef double Met, Sec, Velocity;Velocity speed( Met d, Sec t ) { Velocity v; v = d / t; // ok v = 1 / t; // warning v = (3.5/t) * d; // ok v = (1/(t*t)) * d * t; // ok return v; // ok }Example Output 11 Velocity speed( Met d, Sec t ) 12 { 13 Velocity v; 14 v = d / t; // ok _ 15 v = 1 / t; // warningWarning 632: Assignment to strong type 'Met/Sec' in context: assignmentWarning 633: Assignment from a strong type '1/Sec' in context: assignment 16 v = (3.5/t) * d; // ok 17 v = (1/(t*t)) * d * t; // ok 18 return v; // ok 19 }A quick tutorial on strong typesStrong types are a powerful feature within PC-lint/FlexeLint that enables your program to specify via options that some or all typedef types are finnicky about what type they may combine with. You will notice in the above example that the lint option-strong( AcJcX, Met, Sec, Velocity = Met/Sec )was used. This option indicates, among other things, that Met, Sec, and Velocity are strong types. There is the presumption that each will be typedef'ed later in the program, in this case they are each typedef'ed to double on the next line.The first argument to -strong indicates the kind of checking that will be performed on the provided types. "Ac" indicates that values Assigned to each of these types must be the same strong type. The "c" is a softener that indicates that a constant value may be assigned without triggering a complaint.The "Jc" indicates the required behavior when one of these types are Joined with another of these types. The default is that they will follow along with the rules of dimensional analysis but there are other possibilities including "Jn" (dimensionally neutral -- such as revolutions in RPM) and "Ja" (anti-dimensional -- reverts to a simpler system used in earlier versions of our analyzer). In all, there are nine possible suboptions but "Jc" simply means that constants may be freely joined with these three types without altering the strong type.The "X" says that if a value is extracted and assigned elsewhere, the destination must be the same strong type or at least be in the same strong type hierarchy. The "Velocity = Met/Sec" argument indicates how the strong types are dimensionally related. That is, not only is Met/Sec taken to be a Velocity but also, for example, Velocity * Sec is taken to be a Met and (Met*Met) / Velocity is taken to be Met*Sec, etc.By specifying the relationship between pertinent types and the kinds of operations allowed on them, PC-lint/FlexeLint provides the strong type checking and dimensional analysis necessary to prevent the type of mistake that led to the untimely fate of the Mars Climate Orbiter.The above program is available for examination and modification within our on-line demo. We'd like to thank the Barr Group for including a discussion of FlexeLint's dimensional analysis in their recent webinar.