Daphne, Quantifiers, and Verification Concepts – Detailed Lecture Notes

Administrative / Context

• Material reproduced under Section 113 P of Australian Copyright Act 1968; do not redistribute.
• Lecturer continues from previous slide set; objective is to deepen understanding of propositional & predicate logic as preparation for later program-verification topics.

What Daphne Is and Is Not For

• Daphne’s primary purpose → verification of programs (functional & imperative)
  • Upcoming weeks: recursion, induction proofs; later: verifying imperative programs with Jack.
• Current exercises (pure logic, heavy quantifiers) push Daphne outside its comfort zone ⇒ leads to:
  • “Weird” counter-example searches
  • Inconsistent success with ∀ / ∃ reasoning.
• Analogy from student comment: “like using a calculator for something it wasn’t built to compute.”
• Rationale for early exposure anyway:
  • Students need logic foundations before sophisticated verification.
  • Early tool-familiarity avoids learning curve shock later.

Ghost Declarations

• Syntax: prefix any declaration with the keyword ghost
  • ghost var, ghost predicate, ghost lemma, ghost function, etc.
• Semantics:
  1. Visible to verifier – helps prove properties.
  2. Invisible to compiler – stripped from executable.
  3. Attempting to use a ghost entity in compiled code ⇒ compilation error.
• Broader verification literature also uses “ghost” to denote auxiliary state used only for proofs (e.g.
  – modeling hidden counters in a garbage-collector proof).

Type-Error Example & Trigger Warnings

• Common mistake: forgetting to apply a predicate/function.
  • Predicate p : int → bool.
  • Writing p where a bool is expected yields type error “got int→bool”.
  • Correct: p(x) where x : int.
• SMT “trigger” warnings appear; course does not require deep understanding—silence with :trigger pragmas if needed.

Universal Statements with Preconditions

• General syntaxes
  1. Implication guard: forall x:T :: cond(x) ==> body(x)
  2. “Such-that” form: forall x:T | cond(x) :: body(x)
• Worked example (needed guard):

  lemma NonNegAdd()
    ensures forall v:int :: v >= 0 ==> v + v >= v
  {}

• Without v >= 0 antecedent, property fails for negative numbers.
  • Cannot place requires v >= 0 outside a forall because v is bound only inside the quantifier scope.

Hoare Triples & Vacuous Success

• Hoare triple notation: ${P}\;C\;{Q}$
  • If pre-condition $P$ is false, verifier concludes triple true regardless of $Q$ (vacuous proof via $\mathrm{false} \Rightarrow X$).
• Pitfall: erroneous requires false may mask wrong post-condition—verification reports “proved” yet program unsound.
• Real anecdote: large model-checking case study passed all checks because initial condition was unsatisfiable.

Vacuous Truth in Quantifiers

• Implication inside ∀ : $\forall x\in S.\; (P(x) \rightarrow Q(x))$
  • If no element satisfies $P(x)$ or if $S=\varnothing$ ⇒ whole statement true.
• Examples in Daphne

  lemma Vacuous1()
    ensures forall x:int :: x < 2 && x > 5 ==> x*x == x  // contradicting guard
  {}

  lemma Vacuous2()
    ensures forall x:int | x in {} :: x*x == x  // empty set
  {}

Order of Multiple Quantifiers

• Order matters – swapping ∀ and ∃ changes meaning.
• Simple contrast:
  • \forall x\in S.\; \exists y\in S.\; x>y
    – “Each element has some smaller element.”
  • \exists y\in S.\; \forall x\in S.\; x>y
    – “There is a single minimal element.”
• Classroom analogies
  1. Students/Courses enrollment
  • ∀ students ∃ course (enrolled) ⇒ “each student enrolled somewhere.”
  • ∃ course ∀ students (enrolled) ⇒ “one universal course everyone takes.”
  1. Tennis tournament
  • ∀ player ∃ opponent ⇒ “everyone played someone.”
  • ∃ player ∀ opponent ⇒ “one player faced everyone.”
• Complex scenario (Streaming-TV example)
  • Functions
  • inChannel(T,C) – show T appears on channel C.
  • favourite(S,T) – student S listed T as favourite.
  • Sample assertions examined:
  1. $\exists S.\; \forall C.\; \exists T.\; inChannel(T,C) \land favourite(S,T)$
     – “There is a student whose favourites cover all channels.”
  2. $\exists S,C,T.\; inChannel(T,C) \land favourite(S,T)$ (trivially true).
  3. $\exists C.\; \forall S.\; \exists T.\; inChannel(T,C) \land favourite(S,T)$
     – “One channel from which every student picked something.”
  4. $\exists S\neq R, C, T.\; inChannel(T,C) \land favourite(S,T) \land favourite(R,T)$
     – “Two different students share a favourite show on the same channel.”

Negating Nested Quantifiers

• Rule of thumb: move ¬ inward, flip ∀ ↔ ∃.
• Examples
  1. Original: $\forall s.\; \exists c.\; enrolled(s,c)$
     Negation: $\exists s.\; \forall c.\; \neg enrolled(s,c)$ – “some student in no course.”
  2. Original: $\exists c.\; \forall s.\; enrolled(s,c)$
     Negation: $\forall c.\; \exists s.\; \neg enrolled(s,c)$ – “every course has at least one non-enrolled student.”

Valid vs Invalid Argument Schemes (Common Pitfalls)

• Reminder: stick to modus ponens, modus tollens, syllogisms.
• Invalid prototypes discussed:
  • From “All CS students understand logic” & “All math lecturers understand logic” cannot conclude “All CS students are math lecturers.”
  • From “Small courses ⇒ not difficult exam” & “Course is large” cannot infer exam difficulty (fallacy of the inverse).
• Valid exemplar:
  • $\text{Daredevil} \rightarrow \text{Lawyer}$, ¬Lawyer(Karen) ⇒ ¬Daredevil(Karen) (modus tollens).

Proof by Contradiction – Knights & Knaves Puzzle

• Setting
  • Knights = always true, Knaves = always false.
  • Person A says: “B is a knight.”
  • Person B says: “We are opposite types.”
• Reasoning sketch
  1. Assume A is a knight → A tells truth ⇒ B is knight.
  2. B (a knight) tells truth ⇒ “We are opposite” must hold.
  3. Contradiction: cannot both be knights and opposite.
  4. Therefore A is not knight ⇒ A is knave.
  5. A lies ⇒ statement “B is knight” is false ⇒ B is knave.
  6. Both knaves satisfies B’s statement (“We are opposite”) is false—as required.
• Technique: start with assumption, derive contradiction, apply disjunctive syllogism.

Bound vs Free Variables

• A variable occurrence is bound if inside scope of a quantifier; otherwise free.
• Examples
  1. Formula with no quantifier: x + y > x^2 → both x,y free.
  2. \forall x.\; x + y > x^2
  • x bound, y still free (must come from outer context).
  1. \forall x.\; (x + y > x^2) \land x>2
  • x in left conjunct bound; x in right conjunct free because right part lies outside quantifier parentheses.
  1. Nested quantifiers: $\exists x.\; (\forall x.\; P(x)) \land Q(x)$
  • Inner x (in P) bound to inner ∀, outer x (in Q) bound to outer ∃—two distinct logical variables despite same name.
• Careful naming / scoping avoids accidental capture.

Practical Tips & Common Errors

• Always ask: “Is my precondition satisfiable?” to avoid vacuous verification.
• When Daphne flags type-mismatch (int→bool vs bool), check that every predicate/function is fully applied.
• Silence non-critical SMT trigger warnings with :trigger /* comment */, but investigate if proof unexpectedly fails.
• While exploring pure-logic lemmas, remember limitations; failures may stem from tool heuristics, not logical falsehood.

Connections & Significance

• Logical rigor (quantifiers, negations, Hoare triples) underpins all later material: loop invariants, recursive correctness proofs, data-structure specifications.
• Ghost constructs and vacuous truths re-appear in real-world verification (e.g. proof of memory safety, concurrency protocols).
• Order-sensitivity of quantifiers parallels concepts in database queries (SQL), type systems (dependent types), and natural-language semantics.

Key Equations & Identities (Quick Reference)

• Equivalence of quantifiers: $\exists x.\,P(x) \equiv \neg \forall x.\, \neg P(x)$
• Guarded universal property: $\forall x.(P(x) \rightarrow Q(x))$ true if ∀x, P(x)=false.
• Hoare triple vacuity: $P=\mathrm{false} \;\Rightarrow\; {P}\;C\;{Q}$ always holds.
• Modus tollens: $(P \rightarrow Q) \land \neg Q \;\Rightarrow\; \neg P$

Suggested Next Steps for Study

• Practise re-writing nested quantifiers into plain English; swap order and observe meaning shift.
• Craft custom “ghost” variables for a small algorithm (e.g. factorial) and watch Daphne strip them on compilation.
• Build intuition for vacuous truth by creating forall statements over empty or contradictory domains.
• Attempt more Knights & Knaves variants; encode in Daphne with boolean predicates IsKnight, Says.