FormalMethods07: Exercise 2

Dear students,

some tips for solving Exercise 2:

1. The precondition of the Hoare triple is not complete. It should
    also include information about the length of a and of b (otherwise
    the ProofNavigator proofs will fail since we are writing in possibly
    invalid positions).

2. The loop invariant should include, apart from the usual conditions that
    variables have not changed and range conditions, the length information
    stated above. The core of the invariant, however, is then a FORALL
    statement about all positions j of b that have already been filled,
    with three cases:
    * j < p => ...
    * j = p => ...
    * j > p => ...
    where in each case you say what b[j] is. The invariant is thus
    rather short and simple.

3. The proofs that the the invariant remains correct after every iteration
    depend on knowledge about "get, put, length, content". If you
    expand, together with the definition of the Invariant, the definitions
    of these constants, the proofs only require scatter and auto.
    If you do not perform the expansions immediately, you have to
    perform manual proof decomposition, instantiation, and at some
   critical points these expansions.

Hope this helps a bit. If the proofs do not run through completely, just
submit them as far as you got.

Best regards, WS