Examination Rules
• Time allowed – Two (2) hours, plus ten (10) minutes reading time.
• Answers to Part A must be written in the answer booklets provided.
• Answers to Part B must be completed on the Lab Computers.
• The Final Examination Questions cannot be retained.
• The Final Examination is Open Book. All paper materials are allowed. This includes any piece of paper or book whatsoever, without exceptions. You may bring your own notes – handwritten or otherwise, textbooks, printed materials, practice questions, and so on.
• No paper materials may be removed from the exam room.
• No electronic devices – apart from the Lab Computers – are permitted.
• No talking or communicating with other students in the examination room is permitted.
• Starter files for all the questions in Part B are provided on your lab machines. Do not change the name of the starter files, and make sure to save all your files before leaving the examination hall. A pocket reference sheet for Dafny’s syntax is also provided.
• You are not allowed to edit the provided Dafny definitions or signatures in Part B. For instance, if a lemma statement has {:induction false}, you are not allowed to remove it. You may add additional functions, methods or lemmas to solve the problems if needed.
• For Part B, Visual Studio code with Dafny extension is provided on lab machines. Dafny is also accessible from the command line, for example dafny verify filename.dfy. 1
• For part B, correctness of your solution along with successful verification without warnings or errors will be used as the marking criteria.
Marking Criteria
• The Final Examination is a hurdle task for the Course.
• The hurdle for the Final Examination is a grade of 50% in the Final Examination.
• Failure to achieve a grade of 50% or higher for the Final Examination will mean that you will fail the Course.
• To achieve a grade of 50% or higher in the Final Examination, a score of 50% or higher must be achieved in both Part A and Part B of the Final Examination.
Hi everyone! I hope that your study week is going well : )
All best,
Seb
Good afternoon everyone,
Your final exam is approaching, and the exam structure is as follows:
Part A - Logic
Part B - Dafny
Part A contains five questions worth ten marks each.
Part B contains five questions worth ten marks each.
Part A will test students' understanding of intensional logic, proofs in intuitionistic logic, Lamda Calculi/type theory, sequent calculi, and the Curry-Howard Correspondence.
Part B will test students' understanding of programming, proofs, and verification using Dafny.
Examination Rules:
Marking Criteria: