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.
2015-Nov-25: When exactly is the project submission deadline?
Your projects are due by the end of Friday 27th November. I will not, however, be checking submissions until 9am on Saturday 28th November, and will accept anything received before then as being on time.
2015-Nov-24: Boogie keeps timing out on our program, even when we use the `/useArrayTheory` flag. What can we do?
It's difficult to say for sure why it is timing out: sometimes the underlying SMT solver gets tied up when the verification conditions become very complex.
One thing you can try doing is splitting your Boogie program into separate files. For example, you could have a file for quick sort and a file for bucket sort (since bucket sort relies on quick sort, you could simply include the signature and contracts of the latter and leave them unverified in that file). This should help to reduce the strain on the SMT solver, and might help in isolating the part of your program it is having trouble with.
2015-Nov-17: My Boogie program verifies, but I don't think it should. What's going on?
This might be due to conflicting assumptions: in such scenarios, Boogie can logically deduce false, and then use this to prove any postcondition (false implies everything!). A quick check would be to add ensures false to the postconditions of your procedures (Boogie should not be able to verify them), and use assert false within the procedure bodies to work out where the problem occurs.
2015-Nov-17: Do we need to prove termination?
No.
2015-Nov-15: In Boogie, I can prove that the output is a permutation of the input, but only when postulating via an axiom some "obvious" and isolated sub-property that I'm unable to prove. Is this OK?
If your proof depends on some isolated sub-property that for some reason you cannot prove, then it is more transparent to "factor it out" as a lemma and leave that unproven. Please make sure to document this carefully in your code and report.
2015-Nov-12: Are there any tools that help us to understand failed verification attempts in Boogie?
You might want to have a look at Boogaloo (see the web interface and wiki). Note that this is a research tool: it might not scale up to the Boogie programs you are constructing for the project.
2015-Nov-10: In Boogie, is it possible to modify the arguments of procedures?
No. You can however modify any out parameters (see e.g. r in the McCarthy 91 example), or global variables when a modifies clause is given (see e.g. a in the Bubble Sort example).
2015-Nov-10: In Bucket Sort, how should we distribute the elements across the three buckets? The algorithm suggested on Wikipedia seems quite complicated.
You could distribute elements according to their values. For example, since Bucket Sort is only triggered when all elements are in the range -3N to +3N, you could divide this into three subranges and allocate each one to a bucket.
2015-Nov-02: In AutoProof, are we allowed to use two-step verification?
During debugging, sure; but submitted solutions that verify only with two-step verification enabled are unlikely to receive full credit.
2015-Nov-02: Why can't we prove obvious invariants about arithmetic such as invariant (exists i: int :: i == 5) in Boogie?
The underlying prover has idiosyncratic support for arbitrary first-order integer arithmetic, especially when quantified variables are not expressed in relation to program variables—as in this example. (This should not be a limitation for the project: Boogie should be able to cope with the kinds of invariants that are typically specified for sorting algorithms.)
2015-Oct-30: Can we model the buckets in Boogie as three separate integer maps, or do we need to model them in a more general way?
It's completely fine to model the three buckets as three separate integer maps. (This would be much simpler to deal with than, say, modelling buckets as a map of maps.)
2015-Oct-27: I added check lst.sequence[x] = lst.sequence.old_[y] end and check lst.sequence[y] = lst.sequence.old_[x] end immediately after the call to swap (x, y) in swapper, but they don't pass in AutoProof despite being the postconditions of swap. Why not?
Note that old in the postcondition of swap refers to the pre-state of swap, but old_ in these checks refers to the pre-state of swapper. You may need to strengthen the loop invariant of swapper for them to pass, e.g. by capturing the relationship between elements of lst at any point of the iteration and the elements of lst in the pre-state of swapper.
2015-Oct-20: What do old and old_ mean in AutoProof?
Postconditions of routines can use the syntax "old" to look up the value of an expression in the pre-state, i.e. the state as it was at the beginning of the routine (when the precondition was evaluated). Unfortunately, Eiffel does not allow old expressions to be used in the body of the routine (e.g. loop invariants), so AutoProof provides an additional ghost query "old_" that can. See Section 2.7 of the AutoProof tutorial for more information.
(Note that old_ also refers to the pre-state, and not the state immediately prior to a particular instruction.)
2015-Oct-14: I'm only able to verify Quick Sort using assume statements; is this OK?
You shouldn't need to use assume statements outside of debugging. Be very careful using them! If you assume conflicting properties, it becomes possible to deduce that false holds and thus prove any property at all. If you can verify assert false then something has definitely gone wrong.
2015-Oct-12: I'm struggling to work out how to specify in Boogie that an array is a permutation of another. Any advice?
It might help to inspect how permutations are specified in Microsoft Research's example Boogie program for bubble sort. Note that they rely on using ghost code for computing the perm map. (Note also that this is not the only way to specify permutations in Boogie.)
2015-Oct-07: The Boogie verifier is failing to terminate on my program. Any ideas?
Try using the Boogie flag `/useArrayTheory` (you'll need the offline version to do this).
2015-Oct-07: Out of interest, is there a way to look at the Boogie code that AutoProof is generating?
Yes, by using the flag -nadia.
2015-Oct-07: 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 SV_AUTOPROOF class is already annotated with all the wrapping-related assertions it needs; you shouldn't need to add to, remove, or alter them.
If you're curious to know more, then the tutorial has all of the details. But you don't need these advanced reasoning mechanisms for SV_AUTOPROOF.