[ew:bs] Do some clarifications and fixes
[ew:bs] Do some clarifications and fixes

- note ProverResult as return type and its contents
- add reference to checkProgram to program specification description
- add non negativity predicate to array index assertion
- fix array index in axiom A2
- add references to the interfaces FormulaGenerator and FormulaCompiler
  to note on use of design pattern Strategy

team-worthwhile/worthwhile,team-worthwhile/worthwhile