Experiment 1 [Gries 81]:
Recover formal specifications
// Sum array b of length n into
// variable s
i := 0; s := 0;
while i ¹ n do
  { s := s+b[i];  i := i+1 }
Precondition: n ³ 0
Postcondition:  S = S0 £ j < n b[j]
Loop invariant:
 0 £ i £ n  and  S =  S 0 £ j < i b[j]
[Don’t go too fast.]

Important:  Daikon successfully recovered the formal specifications from all the formally-specified programs in the first two chapters (chapters 14 and 15) that contain such programs.  Conclusion:  I succeeded.

The point of using these programs to test the tool is to know what the result should be:  I have a gold standard for validating the output.

This is an example simple enough to fit on a slide.

Emphasize that the precondition, postcondition, and loop invariant come from Gries; it’s our goal to discover them.