2013-Nov-27: We wondered whether the exact project deadline is today or Thursday 23:59?

It's absolutely fine to submit your project on Thursday (i.e. the latter option).

2013-Nov-27: Verification of my Eiffel program fails, even though it appears to be a trivial application of the rule of consequence. Am I doing something wrong?

Julian: the quick answer to your problem is, that this is a limitation of AutoProof, that does not allow adding triggers to quantified expressions, and has limited support for framing. So if your quantified expression is too difficult, then Boogie might not find a witness to instantiate the quantified expression, or if there are intermediate calls that do not handle framing, then it is not possible to reason about it as well.

2013-Nov-22: We have found out that the Boogie flag `/useArrayTheory` is necessary for the verification of our program. Without the flag merge sort alone and bucket sort alone do verify, however when both are composed Boogie/z3 fail to terminate. The other teams might find this information useful.

Thanks very much for sharing this tip!

2013-Nov-20: Suppose you have a class with two (integer) array attributes, and a method that modifies only one of them (within the body of a loop). How do you prove that the method does not change the other array in any way?

Unfortunately this is not currently possible in AutoProof on account of two deficiencies: one in the language (i.e. Eiffel), and one in the tool. The deficiency in Eiffel is the fact that you cannot use the "old" keyword in postconditions about arrays (hence you cannot express that an array in the post-state is the same as the one in the pre-state). The deficiency in AutoProof is the current lack of support for framing.

If you cannot find another way to verify anything "interesting" about your implementation of the sorting algorithms, then in the report, please do discuss what you were intending to verify, how you planned to do it, why AutoProof wouldn't support it, and how you were able to use the finer-grained control in Boogie to be able to do it.

2013-Nov-17: How much of the Eiffel program are we supposed to translate faithfully to Boogie? For example, should the sort implementations operate on the heap?

You don't need to encode the object-oriented semantics of Eiffel in Boogie. Instead of Eiffel arrays, you can use Boogie's maps as the basic data structure, and reimplement the sorting algorithms using global variables, functions, and procedures.

2013-Nov-17: Can we assume that sequence will not grow?

Yes, it is fine to assume this (see below).

2013-Nov-17: I get segmentation violations when using valid_index(k) in preconditions... is this intended behaviour?

Segmentation violations imply a bug in the tool I'm afraid (feel free to discuss such difficulties in your reports). You can get around this problem however by asserting that k is a value inclusively between 1 and the count of the array. Take a look at some of the example programs in this directory that prove properties about arrays.

2013-Nov-14: AutoProof is giving several "index_in_bounds may fail ..." warnings and cannot verify simple methods!

Check not only the contracts of those methods, but also the contracts of methods they call. Do they involve loops? Have you expressed loop invariants about array bounds? There is some example Eiffel code involving arrays in this directory that AutoProof can verify. They may help you strengthen your contracts and loop invariants enough to eliminate these warnings.

2013-Oct-23: Is it true that the report is only worth 2 marks?

No! The report is worth much more: report writing is intertwined with most of the verification tasks (for example, "describe which parts of the specification you could not verify"; "discuss any implementation choice you evaluated at this point", and so on). The two marks mentioned in Section 3.4 are bonus marks for the quality of writing, not for the content as a whole.

2013-Oct-23: Regarding the line "between -3N and +3N" in the project text, is "between" intended to be inclusive or exclusive?

It doesn't really matter: if I had to pick, then let's say inclusive, but both interpretations would be regarded as equally valid.

2013-Oct-23: Do lists need to be extendable?

It is not a necessary requirement, but they can be. Though in terms of software engineering concerns, it is preferable to have a design to which one can easily add such extra features, than a design that is strictly tied to non-extendable lists and would need to be completely re-engineered.