To stimulate and unify the discussions, we developed a common example that was addressed by the speakers and participants. Here is a sample pseudo code that implements the functions described in the example. Please note that the pseudo code has not been compiled or checked in any way by a software tool. The code has been seeded intentionally with a few defects and other aberrations (just to make it interesting!). The required behavior is specified on the first page of the pseudo code along with assumptions.
We encouraged the participants to approach this example from various angles and varying levels (e.g., actual code vs. formal model vs. assurance case).
This example involves a variety of different kinds of complexities
which are an opportunity to demonstrate the flexibility of a theorem
proving approach, e.g., reasoning about timing relationships,
arithmetic calculations, and non-trivial decision logic.
A preliminary list of questions and comments which were addressed by the participants in the context of this example is given below.