A2 Tips
START THE ASSIGNMENT NOW!
This assignment is more challenging than A1, you will most likely end up spending more time on this assignment than A1,
so make sure to start now, and to spend ample time working on it.
Question 1
Determine what you need to prove in order to show mono is valid. How can you now write this out in Dafny? Can
you use any mathematical techniques you have learnt previously in order to prove it?
Don't forget to add a call to your lemma in the original code (but do not modify the code in any other way!)
Question 2
Read the question carefully, there are some handy tips in the question (such as using the function IsStart).
You cannot use a function in your code, only in your specifications (pre- & post-conditions and invariants) .
Don't forget to use old() as required.
Specification
Make sure to write the specification first. This is the hard part.
Write out everything you need in the specification in words (e.g. for the maximum element in an array, a
postcondition is that "the element needs to exist in the array" which in Dafny we can write as exists i :: 0 <=
i < a.Length && max == a[i]).
It is really easy to underspecify a specification. Make sure to consider any and all edge cases. You can use a test
harness (see Graeme's latest Blackboard announcement) to help assert and show that something is true about
your specification. If something that should assert true but fails, perhaps there is something missing from your
specification.
Make sure to correctly and accurately determine what you can assume about your parameters. Remember that you
can assume the pattern array is non-empty.
You do not need to justify why you need a specific postcondition, but if you add a comment as to what that
postcondition relates to, e.g. "Pattern substitution", it will help you debug, and help the tutors marking easily place
what each set of postconditions are relating to.
Even if your program doesn't verify, still submit the Dafny file (.dfy). You can get marks for having the right
specification, even if your code is incorrect/missing any additional invariants. Most of the marks are associated
with the specification.
Invariants
Go over all the loop techniques you have learnt in class. Which ones can you use?
Do not write any of your invariants without having a method specification. USE THE LOOP TECHNIQUES!!
Do not forget to justify your invariants. What technique from the lecture did you use? Remember that this is like
justifying your predicates in A1 with the rules from the appendix. If you do not comment on how you got your
invariants, you will lose marks.
Code
Write the specification first!
Read the strategy in the assignment spec carefully. Follow it exactly.
If it specifies using X number of loops, only use X number of loops. Not X + 1, not X - 1, X.