Sample invariants
•x,y,z are variables; a,b,c are constants
•Invariants over numbers
–unary: x = a, a £ x £ b, x Ί a(mod b), …
–n-ary: x £ y, x = ay + bz + c,
x = max(y, z), …
•Invariants over sequences
–unary: sorted, invariants over all elements
–with sequence: subsequence, ordering
–with scalar: membership
•Why these invariants?
This is the set of templates for invariants.
Be specific about sequence invariants:  for instance, determining that the elements of an array are sorted or that a particular element is always a member of a collection.

How I came up with these invariants:
•Made up invariants that seemed basic and natural, based on my experience as a programmer
•Analyzed some programs and added invariants that appeared in them and which I believed to be sufficiently general to appear in, and be helpful for understanding, other programs as well
[This is not so different from the way that axioms/lemmas are added to theorem provers (is it?).]

Say how you add new invariants to the system.  The interface is simple:  4 methods instantiate, add_sample, format, confidence.  [But don’t apologize for the lack of a declarative notation.]
I hope that by iterating this process, I will approach a set of universally useful invariants.  There is evidence that I succeeded in obtaining a useful, basic set.  (replace, Weiss).

These can be checked efficiently; see next slide.