Please email any questions regarding the project to chris.poskitt@inf.ethz.ch. Questions and answers relevant to all groups will be anonymised and posted on this page.

2014-Dec-4: In AutoProof, why does the is_equal feature of MML_SEQUENCE return a Boogie type error?

It seems that is_equal is not completely supported by AutoProof yet. Instead of using a.is_equal(b), try a ~ b.

2014-Dec-4: What is expected in terms of comments and the report?

In your Eiffel and Boogie code, a short comment alongside each feature/function/procedure would be very helpful.

The report is for more detailed discussion on the choices, experiences, and challenges along the way to achieving verification of your code. A lot of effort has collectively gone into verifying your programs, but the annotated code alone does not capture this: the report provides a chance to expand on the problems encountered along the way, how you resolved them, why certain specifications/checks/lemmata/implementation choices are necessary, and so on. Furthermore, it allows you to compare the experience of both AutoProof and Boogie to verify the same sorting algorithms. Which tool was better at X? Which tool was more expressive for Y? Which tool was the most productive to work with? Etc. (There are some additional discussion points suggested in Section 3.3 of the project description.)

There are no set restrictions on the form or length of the report, so long as it's well-written, and gets the required points across clearly.

2014-Dec-3: The Boogie verifier is failing to terminate on my specification. Any ideas?

Try using the Boogie flag `/useArrayTheory` (you'll need the offline version to do this).

2014-Dec-3: How close to SV_LIST does our Boogie program have to be?

Let me stress that the aim is not to translate the semantics of an Eiffel program to Boogie, but to specify and verify the same sorting algorithm at the level of Boogie's primitives, functions, and procedures.

2014-Dec-3: If we specify sequence as you suggest, how do we pass it around the sorting procedures?

You don't have to. If you declare sequence, count, N, etc. like this, then they are global, and can be used in the contracts and invariants of procedures without them being passed as parameters. [If you start passing maps (i.e. arrays of integers) to functions and procedures, then you may find yourself writing higher-order assertions — e.g. quantifications over arrays — which are harder to prove in general.]

2014-Dec-2: In Boogie, how should we specify count?

I would suggest keeping it simple, e.g.

	
		// Array elements
		var sequence: [int] int;
		// Number of elements
		var count: int;
		// N constant
		const N: int;

and then focus on the crucial (and most challenging) part, i.e. proving correctness of the sorting algorithms. (Remember that you do not need to specify the heap.)

2014-Dec-1: Can I see how MML_SEQUENCE (and other such classes) are expressed in Boogie?

Sure: the .bpl files you want are in this directory.

2014-Dec-1: We are struggling to define `is_permutation' as a Boogie function. Any advice?

Have you tried defining it axiomatically? See e.g. the axiomatic definition of Fibonacci numbers in Nadia's slides.

2014-Dec-1: In Boogie, do we need to prove functions like `put' and `at'?

The important thing is to implement `sort' in an analogous way (i.e. calling bucket sort or quick sort as according to the project description). If you don't need `at' or `put' to accomplish this, I don't mind them being omitted from the Boogie program. However you'll obviously need `sequence', `N', etc. Make sure to document such design decisions in the report.

2014-Nov-25: What does status: functional mean?

It specifies that the feature contains only a single instruction that assigns a value to Result (see the manual entry).

2014-Nov-25: Is there a way to look at the Boogie code that AutoProof is generating?

You can, by using the flag -nadia.

2014-Nov-25: We're struggling to prove the permutation property for bucket_sort. Is there another way of expressing relations between arrays?

One group points out that they struggled when using across-loops in specifications. An alternative approach is to use the features defined on MML_SEQUENCE, e.g. concatenation, front, and tail.

2014-Nov-25: Do we need to prove anything about the is_permutation feature?

No. The intension of the feature is to use it in the specifications of other features, and you don't need to prove anything about is_permutation itself.

2014-Nov-25: Should the put feature overwrite existing values?

Yes. (Note that lists do not need to be extensible, so this will always be the case.)

2014-Nov-25: What does the status: lemma flag mean in lemmata?

The status: lemma flag disables some of the AutoProof defaults. In particular, lemma features have no automatic unwrapping and wrapping of the Current object, and the code is implicitly ghost code (in the sense that it is code added only for the purpose of specification and verification).

2014-Nov-21: If you label a loop invariant with assume, then AutoProof produces a type error. Is this behaviour intended?

This is because assume is a special tag that allows you to temporarily specify facts for the verifier to use, e.g. in debugging. See the manual entry.

2014-Nov-21: AutoProof is reporting a frame_writable violation. What does this mean?

To fix this problem for a routine X, I would suggest checking that the modifies clauses in loop invariants of X, and any routines that X calls, are encompassed by the modifies clause of X.

2014-Nov-15: Why does AutoProof verify across 1 |..| b.count as X loop check ... end end when the check should fail?

The across loop is not supported by AutoProof and hence is completely ignored (which is why it is able to "verify" it). It does, however, have some support for across expressions. See the language support section of the AutoProof manual for more details.

2014-Nov-14: I'm struggling to get AutoProof to prove that the sorted list is a permutation of the original, despite extensive preconditions, postconditions, and loop invariants involving is_permutation.

This is certainly the most challenging part of the verification. Even if the specifications are correct, AutoProof might still need additional information to be able to mechanically deduce it. Try adding check clauses to the body of your code, or even adding lemmata (see sum_and_max for an example).

2014-Nov-14: Is there a push_back-like feature we can use for sorting elements into buckets?

I would suggest initialising the buckets as empty SIMPLE_ARRAYs and adding elements using force. See also the class reference.

2014-Nov-12: Should sequence return an ARRAY or a SIMPLE_ARRAY?

It should return a SIMPLE_ARRAY (as the class ARRAY from EiffelBase is currently not supported by AutoProof). Apologies for any confusion.

2014-Nov-12: AutoProof is complaining about loop variants, even though we don't specify any. How do we fix this?

AutoProof, by default, will try to prove termination by automatically generating loop variants. When it is unable to do so, it will complain until a suitable variant is manually provided. Since we do not require a termination proof in the project, you can simply disable termination checking by adding decreases([]) to the loop invariant.

2014-Nov-12: 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.

2014-Nov-12: Do lists need to be extensible?

No, this is not required (but they can be).

2014-Nov-10: What are the default annotations that AutoProof uses, and how do they interact with the error messages and warnings?

Response by Julian:

AutoProof reduces the annotation overhead by having default preconditions, postconditions, and modifies clause. To clarify, here is a routine with all the implicit defaults added explicitly:

r (a: ANY)
  require
    default_is_wrapped: Current.is_wrapped -- default "contracts"
    arg_a_wrapped: a.is_wrapped -- default "contracts"

    modify (Current) -- implicit modifies clause
  do
    unwrap  -- default "wrapping"
    ...
    wrap -- default "wrapping"
  ensure
    default_is_wrapped: Current.is_wrapped -- default "contracts"
    arg_a_wrapped: a.is_wrapped -- default "contracts"
  end

The defaults can be removed by adding a note explicit: contracts, a note explicit: wrapping, or by providing a different modifies clause. When overriding a default you should always consider if you need to do some parts manually and explicitly or if it affects other defaults. If you write for example modify (a) as a modifies clause, the implicit modifies clause modify (Current) is overridden and the Current object is not writable anymore. This will lead to a frame violation in the implicit unwrap that you can fix by writing the modifies clause as modify (Current, a) (making explicit that you want to modify the Current object), or by disabling the implicit "wrapping" (i.e. disallow modifications of the Current object and any owned objects).

2014-Oct-31: What do assertions like a.is_wrapped mean to AutoProof?

Object wrapping is an advanced feature of AutoProof that supports reasoning about certain kinds of class invariants. A key problem in reasoning about invariants is deciding when they should hold for an object. The most obvious answer is immediately before and after the execution of any of its methods; but then what about, for example, methods that make recursive calls, where it might be necessary to temporarily "break" the invariant in-between steps? (It gets even more tricky when you start to consider invariants that capture inter-object dependencies, such as those in the observer and iterator design patterns.)

Roughly speaking, you can think of the assertion a.is_wrapped as meaning that object a is in a "consistent" state, i.e. that the invariant should hold and should be checked. The given class invariant for SV_LIST is fortunately rather simple, and should never be temporarily broken during any method call (since sorting should not change the size of array, and should not ever make it Void). As a result, you can use is_wrapped in your preconditions, postconditions, and loop invariants, and AutoProof will be happy. (The skeleton class already has is_wrapped in the pre- and postconditions where AutoProof expects it, but you may need to add it to some loop invariants.)

If you're curious to know more, then this research paper has all of the details. But you shouldn't need these advanced reasoning mechanisms for SV_LIST.

2014-Oct-30: Is it possible to execute tests on SV_LIST? The classes SIMPLE_ARRAY and MML_SEQUENCE are not part of standard Eiffel.

Unfortunately, the SIMPLE_ARRAY and MML_SEQUENCE classes are specification classes used by AutoProof that have dummy implementations. Hence, even if you were to extract them, it wouldn't be possible to run tests that make sense.

I would suggest working in one of two ways. Either:

(1) skip the tests and start verification right away with AutoProof. (While it may seem odd to be verifying code that you're not executing, it's akin to developing a Boogie-style program but in the object-oriented paradigm.)

or, (2) develop a version of SV_LIST that uses standard Eiffel library classes (i.e. ARRAY), do your tests, and then later replace them with the specification classes (SIMPLE_ARRAY etc.) of AutoProof to do verification. Note however that there is no extra credit available in the project for developing tests.

In both cases, the AutoProof manual should be quite helpful (note in particular the class reference page and verification examples).

2014-Oct-16: Why does the SV_LIST skeleton class contain features that are not described in the hand-out?

Take them as "hints" – features that are likely to prove useful, but are not strictly necessary should you prefer to complete the task in a different way.

2014-Oct-16: Why does this program verify in Boogie?

This is due to a bug that occurs when a loop is preceded by the assignment of a negative number to a variable. Note that the bug only occurs in the Rise4Fun version of Boogie; the latest offline version does not exhibit it.

Update (23.10): this appears to have been fixed.