analysis

Checking invariants

•For each potential invariant:

–Instantiate

•That is, determine constants like a and b in y = ax + b

–Check for each set of variable values

–Stop checking when falsified

•This is inexpensive

–Many invariants, but each cheap to check

–Falsification usually happens very early


	All three steps are inexpensive: instantiation, checking, and number of checks (most checks fail quickly).
	There are many invariants, but each one is cheap.

	Can think of the property as a generalization from the first few values; then check the rest of the values.
	Example: 2 degrees of freedom in y=ax+b, so two (x,y) pairs uniquely determine a and b. (I don’t actually do it that way for reasons of numerical stability, but that is the idea.)