Dafny Verification and Formal Methods Exam Review

Dafny Concepts and Preconditions

Preconditions are required; postconditions are ensured.

Methods do not change given parameters unless a modifies clause is present.

Old(E) has the value of E at the start of the method.

Fresh(E) as a postcondition shows that E was created by M.

With if statements, Dafny works normally. With if-case statements, you introduce nondeterminism (hard; you need to prove all options).

Classes have instance variables and methods, which need clear contracts.

A trait is an abstract class, from which classes inherit (like a template in Java). Example: trait A; class B extends A

Class invariants must hold before and after any method. Use ghost predicate Valid().

Behavioral Subtyping: When a class A inherits from another class/trait, the inheriting class is a subtype. This implies Liskov Substitution Principle.

Hoare Triple: Written {P}S{Q}, where P is the precondition, S is the statement, and Q is the post-condition. When execution of S starts in P, Q will hold, i.e., P ⇒ WP(S, Q).

Proof Obligations (General Structure)

Loop Components

• Guard B: A boolean that tells when to continue with the loop.
• Invariant I: Assertion that holds during the loop.
• Frame: What is possibly changed by the loop (implicit, comparable to explicit modifies). Contains all local variables that change.

Loop Invariant Techniques

Invariants need to hold at the beginning and end of each loop iteration.

Data Types and Collections

Exam Review: Theory and Weakest Preconditions

Exam 2025: Theory

1. Hoare Logic Sequential Composition

• Q: Given {P0} S0 {Q0} and {P1} S1 {Q1}, what is minimally needed for {P0} S0; S1 {Q1}?
• A: Q0 ==> P1. (Minimal condition: P0 ==> WP(S0, WP(S1, Q1)))

2. Weakest Preconditions (WP)

• a. Basic Assignment: Q: Calculate wp(x := x + 1, x > 0). A: x + 1 > 0, simplifies to x > -1 (or x >= 0 if x is nat).
• b. Assignment with Quantifier: Q: Calculate wp(n := n + 1, forall i :: 0 <= i < n :: a[i] >= 0), given b == (forall i :: 0 <= i < n :: a[i] >= 0). A: (forall i :: 0 <= i < n + 1 :: a[i] >= 0), which is b && a[n] >= 0.
• c. Sequential Assignment: Q: Calculate wp(p := p + 2; q := p + q, p > 2 && q == 2*p - 4). A: p > 0 && q == p - 2.
• d. Conditional Assignment: Q: Calculate wp(if a > 0 {b := a} else {b := -a}, b == abs(a)). A: true.

Exam 2025: Finding the Influencer (Elimination)

• a. Uniqueness: If a and b are distinct influencers (a != b), then b implies follows(a, b). Since a is an influencer, !follows(a, m) for all m, so !follows(a, b). Contradiction. Influencer is unique if it exists.
• c. Implementation (Elimination Hint):

  method FindInfluencer() returns (c: Member) requires HasInfluencer(0, N-1) ensures IsInfluencer(c) {
    var p := 0, q := N-1; // Candidate range [p..q]
    while p < q
      invariant 0 <= p <= q < N
      invariant HasInfluencer(p, q) // Influencer exists in [p..q]
      decreases q - p
    {
      if follows(p, q) { // p follows q, so p cannot be the influencer.
        p := p + 1;
      } else { // p does not follow q, so q cannot be the influencer.
        q := q - 1;
      }
    }
    c := p;
  }

Exam 2025: Magic Square Specifications

• a. Square Grid Predicate:

  predicate square(g: Grid) {
    |g| > 0 && forall r :: 0 <= r < |g| ==> |g[r]| == |g| 
  }

• c. Main Diagonal Sum:

  function maindiag(g: Grid): nat
    requires square(g)
  { 
    if |g| == 0 then 0 
    else g[|g|-1][|g|-1] + maindiag(g[..|g|-1]) 
  }

Exam 2025: Termination (Decreases Clause)

• a. Tree Recursion: decreases t (if structure shrinks).
• b. Simple Loop: For while n != 0, use decreases n.
• c. Nested Loop: For outer loop changing m and inner loop changing n: decreases |a| - m, |a[0]| - n (Lexicographic order).

Exam 2025: Rectangle Resize

class Rectangle {
    var height: real
    var width: real

    ghost predicate Valid() reads this { height > 0.0 && width > 0.0 }
    function area(): real reads this requires Valid() { height * width }

    method Resize(factor: real)
      requires Valid() && factor > 0.0
      modifies this
      ensures height == old(height) * factor
      ensures width == old(width) * factor
    {
      height := height * factor;
      width := width * factor;
    }
}

Proof sketch for assert area() == 28.0 from area() == 7.0 and Resize(2.0): New area = old(area()) * factor^2 = 7.0 * 2.0^2 = 28.0.

Exam 2024 Review Highlights

1. Hoare Logic

• If {P} T {Q} and {R} T {S}, then {P ∧ R} T {Q ∧ S} holds.
• {¬P} T {¬Q} is not valid in general (contraposition does not apply directly).

2. Dafny Method Contract & Loop Frame

• If an array a is modified, modifies a is required in the contract.
• Loop frame must list all modified variables (e.g., a, index, s).

3. Weakest Precondition (WP) Examples

• x := x-1; {0 ≤ x < 10} ⇒ Pre: 1 ≤ x ≤ 10.
• a := a+b; b := a+b; a := a+b; {a=2A+3B ∧ b=A+2B} ⇒ Pre: a=A ∧ b=B.

5. Zero-Sum Pair in Sorted Sequence (Two Pointers)

method FindZeroPair(a: seq<int>) returns (k: nat, l: nat)
  requires sorted(a) && exists i,j | i<j :: a[i]+a[j]==0
  ensures a[k]+a[l]==0
{
  k, l := 0, |a|-1;
  while k < l && a[k]+a[l] != 0
    invariant exists i,j | k<=i<j<l :: a[i]+a[j]==0 // (Simplified invariant)
  {
    if a[k]+a[l] > 0 then l := l-1;
    else k := k+1;
  }
  // If loop terminates because k=l or a[k]+a[l]==0, the result holds.
"

7. Termination Measures

• Binary Search (recursive): decreases hi - lo (shrinking interval size).
• Zero Check Loop (checking s[i] == 0 up to n): decreases |s| - n.
• Loop with Two Counters (e.g., x decreasing, y increasing towards z): Use lexicographic order: decreases z-y, x.