Course Feedback, Daphne Verification, and Exam Preparation (Comprehensive Notes)

Context and purpose of the session

• Class reps provided feedback; the lecturer thanks them and emphasizes the course is in transition and responsive to student input.
• A survey will be released to collect anonymous student opinions.
• The lecture aims to communicate how feedback is being addressed, both immediately and in the long term.
• Dirk (the co-instructor) is involved behind the scenes and will be introduced next week.
• The course has evolved from last year (Daphne introduced for the first time last year; this year Daphne is used throughout, with significant topic changes and removals).

Immediate, on-going actions (short-term changes)

• Mini assignments and quizzes: students want timely feedback and solutions; the team is exploring ways to release assessments earlier while accommodating long extensions (e.g., for elite athletes).
• Official policy and advice from the university will guide what can be adjusted; ideas are being considered but not yet confirmed.
• Feedback delivery: students want clear feedback from tutors beyond just marks. The lecturer demonstrates how to access feedback on Turnitin within the Moodle page:
  • Go to the mini assignment entry and open the submitted item.
  • Click the specific submission to view the feedback panel. Feedback may appear as comments or bubbles attached to specific parts of the submission.
  • If feedback isn’t visible, students should report it; the teaching team will clarify feedback formats to tutors.
• Solutions to mini assignments: solutions for the following week have been promised; in some weeks, solutions may be released promptly.
• Daphne and theory-synthesis: the aim is to strengthen the correspondence between theory and the Daphne proofs rather than simply adding another programming language.

Daphne, the philosophy of the tool

• Daphne is positioned as a tool to augment verification, not as the sole language to learn; the goal is verification proficiency (proving correctness of programs and properties) applicable to any tool or pen-and-paper proof.
• The annotated Daphne file created by Dirk (useful for understanding how to map paper proofs to Daphne steps) is available in the lecture slide section. It shows, line-by-line, how a paper proof corresponds to a Daphne proof.
• There will be explicit lectures to improve understanding of the correspondence between proofs on paper and Daphne proofs; additional syntax coverage will be included in today’s lecture.
• Daphne is both a programming language and a verification tool (compiler + verifier). The compiler translates code; the verifier proves lemmas and properties. The emphasis here is on the verification side, while ensuring the program compiles.

How to access feedback and how Daphne ties into learning

• Feedback access in Turnitin: tutors provide comments along the submission; students may need to look for speech-bubble style comments or inline notes.
• The lecture notes that Daphne mirrors paper proofs:
  • Paper proofs are the primary reference; Daphne is used to practice the same logical steps with automated feedback.
  • Students should focus on the same inductive structure whether on paper or in Daphne.
• Syntax and understanding: many students struggle with initial syntax and connection to theory; the lecturer will cover basic syntax topics today to reduce confusion.
• The goal is to make Daphne supportive, not intimidating; the teacher notes that for programming-background students, Daphne should augment understanding, not overwhelm with new programming complexity.

Annotated Daphne resource and syntax guidance

• Annotated Dafni/Daphne file (Dirk’s work) is available in the lecture slides; it demonstrates step-by-step how the paper-based induction proof translates to Daphne.
• Daphne syntax guidance is provided via a link to the Daphne website on Woddle; this is a supplementary resource, not a complete course substitute.
• The course includes videos on Daphne syntax and induction proofs; the second video mentions termination (to be covered in Week 8 by Dirk). Don’t panic if that portion is challenging; it’s part of later material.

Starting points for Daphne proofs and how to approach them

• Some students suggested starting from the basics (simple programs to verify invariants) before jumping into logic—this is being considered for future iterations to balance predicate logic understanding with verification.
• For the current approach, the teacher shows how to relate propositional/first-order logic to Daphne, then moves to induction proofs.
• There are two main pathways for induction in proofs:
  • Forward induction (prove p(k) → p(k+1)); base case p(0) must hold.
  • Backward induction (prove p(k−1) → p(k)); requires k > 0 to avoid invalid base cases.

A concrete induction example: sum of integers up to n

• Mathematical identity to prove:
  oxed{orall n ext{ int}, ext{ } n \,\ge\, 0 \ \
  \sum_{i=0}^{n} i = \frac{n(n+1)}{2}}

• Paper-style induction approach (two variants) and their Daphne counterparts:

  • Paper base case: show for $n=0$; left-hand side equals right-hand side (0 = 0).
  • Paper inductive step 1 (k → k+1): assume $pk$ holds; prove $p{k+1}$.
  • Paper inductive step 2 (k−1 → k): assume $p{k-1}$ holds; prove $pk$ for $k>0$.
  • Daphne translation uses a recursive function to model the sum:

  \text{add_all}(n) = \begin{cases}0, & n \le 0 \ n + \text{add_all}(n-1), & n > 0\end{cases}

  • The Daphne proof demonstrates the base case and then uses a recursive call to represent the inductive step, mirroring the paper proof structure.
  • Base case in Daphne: if $n=0$, then add_all(0) = 0 and the target formula holds.
  • Inductive hypothesis in Daphne: assume add_all(n-1) holds; show add_all(n) holds, leading to sum up to n equaling $n(n+1)/2$.

• The lecture explains two presentation styles in Daphne:

  • Style A: use a lemma with a postcondition and a recursive proof that matches the paper steps, including explicit base and inductive steps.
  • Style B: avoid explicit k/ k−1 notation and instead operate with the same variable names (n) and use preconditions (requires) to express domain constraints, then rely on a recursive function to express the induction step.

• The induction proof in Daphne may show partial proof steps; Daphne can prove some steps automatically, but students should be able to write more than Daphne requires and still receive verification.

Practical Daphne concepts and translation guide (high-level)

• Core idea: translate paper proof steps into Daphne constructs (lemma, postcondition/ensures, inductive hypotheses, base case, inductive step).
• Propositional logic and first-order logic mapping:
  • Booleans P, Q; base-type declarations like Boolean variables.
  • Not, implies, and other connectives map to Daphne operators (e.g., not, implies, and conjunction). The instructor shows how to translate a simple lemma with booleans into Daphne syntax.
• Induction specifics:
  • When using k−1 or k, the base case must ensure there is a valid predecessor (hence why sometimes k > 0 is used rather than k ≥ 0).
  • The inductive hypothesis is used to replace the left-hand side with the right-hand side in the proof, mirroring algebraic simplification in the paper version.
• Recursive functions in Daphne:
  • Example: add_all(n) defined recursively to accumulate the sum; the proof then demonstrates equivalence to the closed form using algebraic manipulation and the inductive hypothesis.
• The role of the proof structure:
  • Each step of the proof on paper has a corresponding step in Daphne; Daphne serves as a structured, checkable proof assistant rather than a separate math language.
• Terminology recap (as referenced by the lecturer):
  • Postcondition (ensures): what must hold after the function/proof finishes.
  • Inductive hypothesis: the assumption that the property holds for a smaller or previous case.
  • Inductive step: demonstrating that if the hypothesis holds for a case, it holds for the next one.
  • Base case: the starting case where the property is directly shown.

Final examination format and scope (context from last year’s paper)

• Exam structure (as per last year’s paper used for guidance):
  • Duration: $3\text{ hours} \; + \; 15\text{ minutes reading time}$
  • Format: in person, closed book; you may bring a two-page (two-sided) notes sheet.
  • Daphne content: no Daphne questions in the final exam or quizzes; Daphne learning outcomes are tied to mini-assignments only.
  • The exam covers multiple topics: propositional logic, first-order logic (predicate logic), structural induction, list induction, termination (to be covered by Dirk later in Week 8), and whole logic.
  • The final exam will not include automata diagrams (NFAs/DFAs) or grammar-heavy content; those topics were removed from the current course content.
• Exam preparation guidance:
  • Tutorials include non-definite (open) questions to practice writing proofs on paper, mirroring the Daphne approach.
  • The current and upcoming weeks will align the exam content with the course’s updated learning outcomes; some topics are emphasized in different components (some outcomes are exclusive to the final, some to quizzes, etc.).
• Past papers and solutions:
  • Last year's exam paper is available for reference, including the general structure and sample questions; solutions may be provided later depending on staff time. The team will explore releasing worked solutions for past papers where feasible.

Support resources and adjustments (availability and access)

• Drop-ins:
  • Timings were criticized as late; timetabling is being checked to offer alternative times; if not possible, current drop-ins remain as the primary on-campus option.
  • Students are encouraged to attend drop-ins or use Ed to get help when they cannot attend in person.
  • A poll will be released to gather preferred times if alternative slots become feasible.
• Self-study and practice materials:
  • Extra problems on induction and recursive algorithms will be provided as optional practice for students struggling with theory; these are optional and aim to build foundational skills.
  • Discrete mathematics textbooks (library) provide extensive practice problems and solutions for the basic concepts covered in the course.
• Additional topics and resources:
  • A Daphne syntax quick guide is available on Woddle, along with the Daphne website link for supplementary reference.
  • The course includes weekly videos; the second video includes termination, a topic covered later in the course.

Practical study tips and course philosophy

• The core objective is verification proficiency, not mastering Daphne as a programming language per se.
• The Daphne tool should feel like a helpful guide that checks each proof step and points out errors, similar to having a coach over your shoulder.
• If you’re struggling, focus on grounding your understanding in the paper proofs first, then translate to Daphne, using the annotated Daphne file as a bridge.
• Don’t panic about the more advanced termination topic; it’s planned for a later week and will be covered by Dirk.

Summary of key takeaways for exam prep

• Expect the final to focus on: propositional logic, first-order logic, structural induction, list induction, and some aspects of termination/whole logic; Daphne content is not in the final.
• Use the annotated Daphne file to understand the link between paper proofs and Daphne proofs.
• Practice both base cases and inductive steps, including forward and backward induction variants.
• Use drop-ins and library resources for extra problems; engage with the anonymous survey and class reps if you have concerns about the course structure or assessment timelines.
• Remember the overarching aim: develop verification skills that transfer to any verification tool or method, not just Daphne.