The Fluid Project is focused on creating practicable tools
for programmers to assure and evolve real programs. We focus on
"mechanical" program properties that tend to defy traditional testing
and inspection regimes. These are properties with a non-local
character, in that there may be no single place in the code where they
are manifest, and they may involve non-determinism.

We have explored properties including:

• race conditions and locking policies,
• unique references and other programmer-significant aliasing
  properties,
• effects,
• appropriate typing,
• realtime threading policies, and
• single-threading policies.

These properties bear significantly on code safety, security, API
compliance, and other attributes of dependability.

Composable static semantic program analyses are used to assure
consistency of code and programmer expressed "low-level" models of
design intent. Thus a failure to achieve assurance can indicate an error
in the model, an error in the code, or an insufficiently precise
analysis.

In order to facilitate experimentation, our prototype tool is
presented as a seemingly benign plug-in in the widely adopted Eclipse
IDE for Java. Case studies have identified numerous concurrency and
other anomalies in production code drawn from a variety of sources,
including government, industry, and open source.

We are guided in our design by a set of principles related to
practicability. Specifically:

• Incrementality and early
  gratification. Any increment of effort we ask programmers to
  undertake should yield a generally immediate reward in the form of bug
  finding, assurance creation, guidance in evolution, or model expression.
  
• Familiar expression. Properties should be expressed tersely
  and using terminology already familiar to programmers.
• Cut points and
  composability. Components can be assured separately, and the
  assurances linked into chains of evidence.

The principle of incrementality suggests that partial chains are
valuable in that they can assist in localizing attention when there are
problems.