The final examination will take place on 23 April at 9 am in the Sports Complex.
Recall that the examination is open book, meaning that you are allowed to use any kind of documentation. Electronic devices are not permitted. You are not allowed to share any material with your colleagues. Here you can find some generic information about open book exams. I strongly recommend that you (a) index well your material so that you can find the information you seek in short order and (b) ignore your material as much as possible (ideally, completely). If you stop every time to look things up you will most likely run out of time. Instead of bringing your textbook and/or lecture notes I also recommend that you prepare a few cheat sheets (no more than 4 pages) summarizing key concepts; this is going to save you considerable time during the exam.
This test covers the matter already covered by the mid-term examination plus the matter discussed in the second half of the term. The latter consists of Chapters 1, 2, 3, 4, and 12 from the textbook and the associated lectures and lecture notes, plus the introduction to formal methods.
The type of the questions on the first half of the course is exactly the same as the type of questions pertinent to the mid-term exam. Make sure you review the mid-term examination section.
Additional questions (covering the second half of the course) will be similar to the ones asked in Assignments 5, 6, and 7, plus some small questions that will test the basic understanding of the concepts. You are encouraged to check out the exercises in the textbook for supplementary practice but you should be fine if you participated in solving the assignment questions. It is worth emphasizing that it is crucial to understand how to answer questions from the assignments, especially the ones in Assignments 6 and 7. Do not forget about Chapter 3, which should be considered a nice set of solved exercises. For additional practice feel free to specify and then verify any kind of code fragments containing loops and manipulating arrays. Code fragments that contain conditionals (with and without else branches) should also be of interest.
Expect the weights of the sections to be roughly 35% formal languages, 10% parsing, 40% algorithm verification, 10% formal methods, and 5% unimplementable specifications.
Just like the mid-term exam the test will be fast paced leaving you little time to check out your notes, hence my advice to ignore said notes as much as possible and to prepare cheat sheets. If the assignment questions were asked in the test then the following are my expectations regarding the amount of time you would need to answer them:
The additional, general knowledge questions will be simple enough to be answerable in 5 minutes (I reserve the right to ask 10-minute questions, but the probability of those is low).
While answering questions related to deductive verification it is worth keeping in mind a few things as follows. The goal of the questions is not to determine whether a correctness statement is valid or not; in most cases this is kind of obvious form the very start. Instead, the goal is to apply a formal proof system to determine the validity of that statement. Such a formal proof system is a collection of axioms and inference rules, and your mission is to systematically apply these axioms and inference rules to prove correctness. Such a systematic application must result in a proof tableau. Nothing else will be marked. In particular, there is no need to informally analyze the code or provide anything else than the tableau; none of this additional information will be marked. The (non-obvious) mathematical facts used should be stated in the tableau itself at the point of first use, except when the respective fact requires an explanation. Such an explanation is the only thing that is expected to appear outside the tableau.
In order to demonstrate that you are capable of applying a proof system (and for me to understand your demonstration) both you and me need to know what is the proof system being used. The easiest (and strongly preferred) way to accomplish this is to use the proof system presented in class. If for some reason you decide to use a different proof system then you must include that proof system somewhere in your exam paper, which means stating all the axioms and inference rules that constitute the system (not just the ones used, all of them). You need to include this description only once (recommended location: the back of the first page in the exam booklet), but you need to tell me where I can find this description in every place that uses it. No marks will be given to any proof tableau that is constructed using a different proof system than the one used in class and that does not contain a pointer to the description of the proof system being used.
When it comes to formal methods, I expect you to be able to write simple CSP descriptions and also to be able to construct the transition graphs of given CSP processes. You are also expected to be able to inspect transition graphs and draw conclusions about the behaviour of the respective system including but not limited to the identification of deadlock situations. Check out the lecture notes for some larger examples (such as Isabella and Kate) and also for the definition of deadlock. Finally, you should be able to compute the set of traces of simple processes and draw conclusions about the equivalence of two processes based on their traces.
I might ask a question on computability, which will be general in nature and will test your overall comprehension of the concepts of unsolvable problems and reductions.
Here are my solutions for the mid-term examination questions.
The test covers formal languages namely, Chapter 7 to Chapter 11 from the textbook and the associated lectures and lecture notes. Sections 8.5 and 10.7 were not covered and so will not be tested.
The type of questions asked in the examination will be similar to the ones asked in Assignments 1 to 4, plus some small questions that will test the basic understanding of the concepts. You are encouraged to check out the exercises in the textbook for supplementary practice but you should already be fine if you participated in solving the assignment questions and you checked (or will check) your answers against mine. Note that assignment 4 will not be marked in time for the examination, but I will post my solutions on the 19th so that you can check them out against yours.
The test will be fast paced, leaving you little time to check out your notes, hence my advice to ignore said notes as much as possible and to prepare cheat sheets. If the assignment questions were asked in the test then the following are my expectations regarding the amount of time you would need to answer them:
The additional, general knowledge questions will be simple enough to be answerable in 5 minutes (I reserve the right to ask 10-minute questions, but the probability of those is low).
Obviously the test cannot cover all the types of questions asked in the assignments. Instead a selection of question types will be asked now, and the rest of the types will be relegated to the final examination.
Recall that the assignments can be done in groups of up to three students. All the collaborators must be currently enrolled in the course. A single joint solution must be submitted for each group, including the names and student numbers of all the collaborators.
Late submissions will be accepted subject to a penalty of 10% per day late until my solutions are posted on the course’s Web site (which can happen as soon as three days after the due date). No submissions will be accepted afterward.
It goes without saying that a correct answer with no justification will give you full marks (unless the justification is explicitly requested in the question), while an incorrect answer with no justification will give you no marks. However, there is also a middle ground: a justification that makes sense may give you partial marks even if the answer in incorrect. I therefore strongly encourage you to provide a justification for your answer even if such a justification is not explicitly requested.