Learning Objectives

• Define propositions and the logical connectives $\neg$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$.
• Construct truth tables for compound propositions.
• Verify logical equivalences (e.g., De Morgan's laws) by truth table.
• Translate logical connectives into Java's !, &&, ||, and conditional expressions.
• Use truth tables to identify tautologies, contradictions, and contingencies.

Concept Overview

A proposition is a declarative statement that is either true or false (not both). Examples:

• "7 is prime" (true)
• "4 is odd" (false)
• "Is this a question?" (not a proposition)

Logical connectives combine propositions:

The implication $P \rightarrow Q$ is the most important and most confusing connective for new students. It is logically equivalent to $\neg P \vee Q$. When P is false, the implication is vacuously true regardless of Q.

Why this matters in CS:

• Conditionals: Every if-else statement evaluates a compound proposition.
• Short-circuit evaluation: Java's && and || don't evaluate the second operand if the result is determined by the first (this has real consequences for null checks).
• Assertions: assert P crashes if proposition P is false.
• Specifications: Method contracts are implications: "if the precondition holds, then the postcondition holds."

Formal Notation

A truth table lists all possible truth values for the atomic propositions and the resulting value of the compound expression.

Truth table for implication $P \rightarrow Q$:

Key equivalences:

• $P \rightarrow Q \equiv \neg P \vee Q$
• $\neg(P \wedge Q) \equiv \neg P \vee \neg Q$ (De Morgan)
• $\neg(P \vee Q) \equiv \neg P \wedge \neg Q$ (De Morgan)
• $P \rightarrow Q \equiv \neg Q \rightarrow \neg P$ (Contrapositive)
• $P \leftrightarrow Q \equiv (P \rightarrow Q) \wedge (Q \rightarrow P)$

Terminology:

• Tautology: always true (e.g., $P \vee \neg P$)
• Contradiction: always false (e.g., $P \wedge \neg P$)
• Contingency: sometimes true, sometimes false

Worked Examples

Example 1: Building a Truth Table — Discrete Math

Problem: Construct the truth table for $\neg P \vee Q$ and show it is equivalent to $P \rightarrow Q$.

The last two columns are identical, confirming $P \rightarrow Q \equiv \neg P \vee Q$. $\blacksquare$

Example 2: Java Translation — Truth Table Generator

public class TruthTableDemo {

    /** Implication: P → Q ≡ ¬P ∨ Q */
    public static boolean implies(boolean p, boolean q) {
        return !p || q;
    }

    /** Biconditional: P ↔ Q */
    public static boolean iff(boolean p, boolean q) {
        return p == q;
    }

    /**
     * Prints a truth table for two propositions.
     * The evaluator takes (p, q) and returns the compound result.
     */
    public static void truthTable2(String label,
            java.util.function.BiFunction<Boolean, Boolean, Boolean> eval) {
        System.out.println("Truth table for: " + label);
        System.out.println("  P     Q     Result");
        System.out.println("  ----- ----- ------");
        for (boolean p : new boolean[]{true, false}) {
            for (boolean q : new boolean[]{true, false}) {
                System.out.printf("  %-5s %-5s %s%n", p, q, eval.apply(p, q));
            }
        }
        System.out.println();
    }

    public static void main(String[] args) {
        // P → Q
        truthTable2("P → Q", (p, q) -> implies(p, q));

        // ¬P ∨ Q (should match P → Q)
        truthTable2("¬P ∨ Q", (p, q) -> !p || q);

        // De Morgan: ¬(P ∧ Q) vs ¬P ∨ ¬Q
        truthTable2("¬(P ∧ Q)", (p, q) -> !(p && q));
        truthTable2("¬P ∨ ¬Q", (p, q) -> !p || !q);

        // Verify equivalence programmatically
        boolean allMatch = true;
        for (boolean p : new boolean[]{true, false}) {
            for (boolean q : new boolean[]{true, false}) {
                if ((!(p && q)) != (!p || !q)) allMatch = false;
            }
        }
        System.out.println("De Morgan's Law verified: " + allMatch);
    }
}

Example 3: De Morgan's Laws — Combined Proof and Code

Problem: Prove $\neg(P \wedge Q) \equiv \neg P \vee \neg Q$ by truth table, then verify in Java.

Columns 4 and 7 match. $\blacksquare$

Java verification:

public static boolean verifyDeMorgan() {
    for (boolean p : new boolean[]{true, false}) {
        for (boolean q : new boolean[]{true, false}) {
            assert (!(p && q)) == (!p || !q) : "DM1 failed";
            assert (!(p || q)) == (!p && !q) : "DM2 failed";
        }
    }
    return true;
}

Example 4: Tautology Check

Problem: Show that $P \vee \neg P$ is a tautology (Law of Excluded Middle).

Always true. $\blacksquare$

Example 5: Short-Circuit Evaluation in Java

Problem: Explain why if (arr != null && arr.length > 0) is safe but if (arr.length > 0 && arr != null) may crash.

Solution: Java's && uses short-circuit evaluation: if the left operand is false, the right operand is never evaluated. So:

• arr != null && arr.length > 0: If arr is null, arr != null is false, and arr.length is never accessed. Safe.
• arr.length > 0 && arr != null: If arr is null, arr.length throws NullPointerException.

This is a real-world consequence of the truth table for &&: if the first operand is false, the result is false regardless of the second operand. Java exploits this to skip evaluation.

Proof Techniques Spotlight

Proof by Truth Table

For propositions involving a finite number of atomic variables, we can verify equivalences exhaustively:

Template:

1. List all $2^n$ combinations of truth values for $n$ atomic propositions.
2. Compute each side of the equivalence for every row.
3. If all rows match, the equivalence is proven.

Limitations: This only works for propositional logic (finitely many cases). For predicate logic with quantifiers (∀, ∃), we need different techniques.

Common mistakes:

• Forgetting that $P \rightarrow Q$ is true when $P$ is false (vacuous truth).
• Confusing $P \rightarrow Q$ with $Q \rightarrow P$ (the converse).
• Confusing "or" in English (often exclusive) with $\vee$ in logic (inclusive).

Java Deep Dive

import java.util.*;
import java.util.function.*;

public class PropositionalLogicLibrary {

    // --- Core Connectives ---

    public static boolean not(boolean p) { return !p; }
    public static boolean and(boolean p, boolean q) { return p && q; }
    public static boolean or(boolean p, boolean q) { return p || q; }
    public static boolean implies(boolean p, boolean q) { return !p || q; }
    public static boolean iff(boolean p, boolean q) { return p == q; }
    public static boolean xor(boolean p, boolean q) { return p ^ q; }
    public static boolean nand(boolean p, boolean q) { return !(p && q); }
    public static boolean nor(boolean p, boolean q) { return !(p || q); }

    // --- Truth Table Engine ---

    /**
     * Generates a truth table for n variables.
     * Returns all 2^n rows as boolean arrays.
     */
    public static boolean[][] allCombinations(int n) {
        int rows = 1 << n;  // 2^n
        boolean[][] table = new boolean[rows][n];
        for (int r = 0; r < rows; r++) {
            for (int c = 0; c < n; c++) {
                table[r][c] = ((r >> (n - 1 - c)) & 1) == 1;
            }
        }
        return table;
    }

    /** Checks if a formula with n variables is a tautology */
    public static boolean isTautology(int n, Function<boolean[], Boolean> formula) {
        for (boolean[] row : allCombinations(n)) {
            if (!formula.apply(row)) return false;
        }
        return true;
    }

    /** Checks if two formulas are logically equivalent */
    public static boolean areEquivalent(int n,
            Function<boolean[], Boolean> f1,
            Function<boolean[], Boolean> f2) {
        for (boolean[] row : allCombinations(n)) {
            if (!f1.apply(row).equals(f2.apply(row))) return false;
        }
        return true;
    }

    /** Pretty-prints a truth table for a formula with named variables */
    public static void printTruthTable(String[] varNames,
            Function<boolean[], Boolean> formula, String formulaName) {
        int n = varNames.length;
        // Header
        StringBuilder header = new StringBuilder("  ");
        for (String v : varNames) header.append(String.format("%-6s", v));
        header.append(formulaName);
        System.out.println(header);
        System.out.println("  " + "-".repeat(header.length() - 2));

        // Rows
        for (boolean[] row : allCombinations(n)) {
            StringBuilder line = new StringBuilder("  ");
            for (boolean val : row) line.append(String.format("%-6s", val ? "T" : "F"));
            line.append(formula.apply(row) ? "T" : "F");
            System.out.println(line);
        }
        System.out.println();
    }

    // --- Demonstrations ---

    public static void main(String[] args) {
        System.out.println("=== Propositional Logic Library ===\n");

        // Print truth table for P → Q
        printTruthTable(new String[]{"P", "Q"},
            row -> implies(row[0], row[1]), "P → Q");

        // Print truth table for ¬P ∨ Q
        printTruthTable(new String[]{"P", "Q"},
            row -> or(not(row[0]), row[1]), "¬P ∨ Q");

        // Verify De Morgan's Laws
        boolean dm1 = areEquivalent(2,
            row -> not(and(row[0], row[1])),
            row -> or(not(row[0]), not(row[1])));
        boolean dm2 = areEquivalent(2,
            row -> not(or(row[0], row[1])),
            row -> and(not(row[0]), not(row[1])));
        System.out.println("De Morgan 1 (¬(P∧Q) ≡ ¬P∨¬Q): " + dm1);
        System.out.println("De Morgan 2 (¬(P∨Q) ≡ ¬P∧¬Q): " + dm2);

        // Check tautologies
        System.out.println("\nTautology checks:");
        System.out.println("  P ∨ ¬P: " + isTautology(1, row -> or(row[0], not(row[0]))));
        System.out.println("  P → P: " + isTautology(1, row -> implies(row[0], row[0])));
        System.out.println("  (P→Q) ↔ (¬Q→¬P): " + isTautology(2,
            row -> iff(implies(row[0], row[1]), implies(not(row[1]), not(row[0])))));

        // Three-variable example: (P ∧ Q) → R
        printTruthTable(new String[]{"P", "Q", "R"},
            row -> implies(and(row[0], row[1]), row[2]), "(P ∧ Q) → R");
    }
}

Historical Context

Aristotle (384–322 BC) developed the first formal system of logic — syllogisms, which are structured arguments with premises and conclusions. His work dominated logic for over two millennia.

George Boole (1815–1864) revolutionized logic by showing that logical reasoning could be represented algebraically. His The Laws of Thought (1854) introduced Boolean algebra, where propositions are variables that take values 0 (false) and 1 (true), and logical operations correspond to algebraic operations.

Augustus De Morgan (1806–1871) formulated the laws that bear his name: $\neg(P \wedge Q) \equiv \neg P \vee \neg Q$ and $\neg(P \vee Q) \equiv \neg P \wedge \neg Q$.

Claude Shannon's 1937 master's thesis showed that Boolean algebra could be used to analyze electrical switching circuits — the foundation of digital computers. Every logic gate in a CPU implements a Boolean function.

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. Is the sentence "This statement is false" a proposition? Why or why not?

A2. What is the truth value of $P \rightarrow Q$ when $P$ is false and $Q$ is false? Explain in everyday terms.

A3. True or false: $P \vee Q$ in logic means "P or Q, but not both." Correct any misconception.

A4. What does short-circuit evaluation mean for && and || in Java?

Slide Set B: Proof Problems

B1. Prove by truth table that $(P \rightarrow Q) \wedge (Q \rightarrow R) \rightarrow (P \rightarrow R)$ is a tautology.

B2. Prove De Morgan's second law: $\neg(P \vee Q) \equiv \neg P \wedge \neg Q$.

B3. Show that $P \rightarrow Q$ is not equivalent to $Q \rightarrow P$ by finding a row where they differ.

Slide Set C: Java Coding Problems

C1. Write a Java method boolean implies(boolean p, boolean q) and test it with all four combinations.

C2. Write a truth table generator that prints the truth table for any binary Boolean function.

C3. Write a method that checks whether a given 2-variable Boolean function is a tautology by testing all 4 rows.

Full Problem Set

Discrete Math Problems

DM1. Construct truth tables for: (a) $P \wedge (Q \vee R)$, (b) $(P \wedge Q) \vee (P \wedge R)$. Are they equivalent?

DM2. Prove that $P \rightarrow (Q \rightarrow R) \equiv (P \wedge Q) \rightarrow R$ using truth tables.

DM3. Which of the following are tautologies? (a) $P \rightarrow (P \vee Q)$, (b) $(P \wedge Q) \rightarrow P$, (c) $P \rightarrow (Q \rightarrow P)$, (d) $(P \vee Q) \rightarrow P$.

DM4. Using only $\neg$ and $\vee$, express: (a) $P \wedge Q$, (b) $P \rightarrow Q$, (c) $P \leftrightarrow Q$.

DM5. Prove that NAND ($\uparrow$, where $P \uparrow Q \equiv \neg(P \wedge Q)$) is functionally complete: express $\neg P$, $P \wedge Q$, and $P \vee Q$ using only NAND.

DM6. Write the negation of: "If it is raining, then the ground is wet" in both symbolic and English form.

DM7. Determine whether these compound statements are tautologies, contradictions, or contingencies: (a) $(P \rightarrow Q) \vee (Q \rightarrow P)$, (b) $P \leftrightarrow \neg P$, (c) $(P \rightarrow Q) \leftrightarrow (\neg Q \rightarrow \neg P)$.

Java Programming Problems

JP1. Implement all 16 possible binary Boolean functions (there are exactly $2^{2^2} = 16$). Print the truth table for each and label it.

JP2. Write a method that takes a BiFunction<Boolean, Boolean, Boolean> and determines if it is a tautology, contradiction, or contingency.

JP3. Implement a BooleanExpression class that represents expressions as trees (with AND, OR, NOT, IMPLIES nodes and VAR leaves). Write an evaluate(Map<String, Boolean> assignment) method.

JP4. Write a program that takes a compound Boolean expression and prints its truth table. Support operators !, &&, ||, ->.

JP5. Implement a method that, given two Boolean expressions, checks whether they are logically equivalent by exhaustively testing all inputs.

JP6. Write a program that verifies De Morgan's Laws, the distributive laws, and the absorption laws by truth table, printing "VERIFIED" or "FAILED" for each.

Bridge Problems

BR1. A method has precondition $P$ and postcondition $Q$. The specification is $P \rightarrow Q$. Explain why the method is "correct" (vacuously) when the precondition is false, and relate this to the truth table for implication.

BR2. Write a Java program that takes a combinational logic circuit (specified as a series of gates: AND, OR, NOT, NAND) and computes the truth table of the circuit. Test with a half-adder circuit (sum = XOR, carry = AND).

BR3. Java's && and || use short-circuit evaluation, but & and | do not. Write test cases that demonstrate the difference (e.g., where one causes a NullPointerException and the other does not). Explain how this relates to the logical equivalence between P && Q and P & Q.

Solutions

Discrete Math Solutions

DM1. Both expressions produce the same truth table (distributive law):

They are equivalent. $\blacksquare$

DM2. Truth table (8 rows) confirms all rows match.

DM3. (a) Tautology: if P is true, then P∨Q is true; (b) Tautology: P∧Q implies P; (c) Tautology: if P then Q→P is vacuously true (P makes Q→P true); (d) Contingency: P=F, Q=T gives F.

DM4. (a) $P \wedge Q \equiv \neg(\neg P \vee \neg Q)$; (b) $P \rightarrow Q \equiv \neg P \vee Q$; (c) $P \leftrightarrow Q \equiv (\neg P \vee Q) \wedge (\neg Q \vee P) \equiv \neg((\neg P \vee Q) \vee ...)$ — more naturally: $\neg(\neg(\neg P \vee Q) \vee \neg(\neg Q \vee P))$... or using only $\neg, \vee$: $(\neg P \vee Q) \wedge (\neg Q \vee P)$ where $A \wedge B = \neg(\neg A \vee \neg B)$.

DM5. $\neg P \equiv P \uparrow P$. $P \wedge Q \equiv (P \uparrow Q) \uparrow (P \uparrow Q)$. $P \vee Q \equiv (P \uparrow P) \uparrow (Q \uparrow Q)$. $\blacksquare$

DM6. Symbolic: $\neg(P \rightarrow Q) \equiv P \wedge \neg Q$. English: "It is raining and the ground is not wet."

DM7. (a) Tautology (try P=T,Q=F: P→Q=F but Q→P=T, so disjunction is T; all rows give T). (b) Contradiction (P↔¬P is always false). (c) Tautology (contrapositive equivalence).

Java Solutions

JP1.

public static void allBinaryFunctions() {
    String[] names = {"F", "AND", "P∧¬Q", "P", "¬P∧Q", "Q",
        "XOR", "OR", "NOR", "XNOR", "¬Q", "P∨¬Q",
        "¬P", "¬P∨Q", "NAND", "T"};
    for (int fn = 0; fn < 16; fn++) {
        System.out.printf("Function %2d (%s):%n", fn, names[fn]);
        for (int r = 0; r < 4; r++) {
            boolean p = (r & 2) != 0, q = (r & 1) != 0;
            boolean result = ((fn >> r) & 1) == 1;
            System.out.printf("  %s %s → %s%n", p, q, result);
        }
    }
}

JP2.

public static String classify(BiFunction<Boolean, Boolean, Boolean> f) {
    int trueCount = 0;
    for (boolean p : new boolean[]{true, false})
        for (boolean q : new boolean[]{true, false})
            if (f.apply(p, q)) trueCount++;
    if (trueCount == 4) return "tautology";
    if (trueCount == 0) return "contradiction";
    return "contingency";
}

JP6.

public static void verifyLaws() {
    boolean[][] rows = {{true,true},{true,false},{false,true},{false,false}};
    // De Morgan 1
    boolean ok = true;
    for (boolean[] r : rows) ok &= (!(r[0]&&r[1])) == (!r[0]||!r[1]);
    System.out.println("De Morgan 1: " + (ok ? "VERIFIED" : "FAILED"));
    // De Morgan 2
    ok = true;
    for (boolean[] r : rows) ok &= (!(r[0]||r[1])) == (!r[0]&&!r[1]);
    System.out.println("De Morgan 2: " + (ok ? "VERIFIED" : "FAILED"));
    // Distribution
    // Need 3 vars for distributive
    for (boolean p : new boolean[]{true,false})
        for (boolean q : new boolean[]{true,false})
            for (boolean r : new boolean[]{true,false}) {
                assert (p&&(q||r)) == ((p&&q)||(p&&r));
                assert (p||(q&&r)) == ((p||q)&&(p||r));
            }
    System.out.println("Distributive laws: VERIFIED");
}

Learning Objectives

• Distinguish between an implication, its converse, inverse, and contrapositive.
• Prove statements using contraposition and contradiction.
• Define universal ($\forall$) and existential ($\exists$) quantifiers and negate quantified statements.
• Translate quantified statements into Java loops and search patterns.
• Use quantifiers to express preconditions, postconditions, and loop invariants.

Concept Overview

Implication and Its Variants

Given the implication $P \rightarrow Q$ ("if P then Q"):

The contrapositive is the key tool: to prove "$P \rightarrow Q$", it is often easier to prove "$\neg Q \rightarrow \neg P$".

Proof by Contradiction

To prove a statement $S$:

1. Assume $\neg S$.
2. Derive a contradiction (something that is always false).
3. Conclude $S$ must be true.

Quantifiers

Negation of quantifiers:

Formal Notation

Nested quantifiers appear frequently:

• $\forall x,\, \exists y,\, P(x, y)$: "For every $x$, there is some $y$ making $P$ true."
• $\exists x,\, \forall y,\, P(x, y)$: "There is some $x$ that makes $P$ true for every $y$."

Order matters! These are generally not equivalent.

Negation of nested quantifiers:

Worked Examples

Example 1: Proof by Contrapositive — Discrete Math

Problem: Prove: If $n^2$ is even, then $n$ is even.

Proof (by contrapositive). We prove the contrapositive: if $n$ is odd, then $n^2$ is odd.

Assume $n$ is odd. Then $n = 2k + 1$ for some integer $k$. So:

Since $2k^2 + 2k \in \mathbb{Z}$, $n^2$ is odd. $\blacksquare$

Example 2: Java Translation — Universal and Existential Checks

public class QuantifierDemo {

    /**
     * Universal quantifier: ∀x ∈ arr, predicate(x) is true.
     * Java pattern: loop through all, return false on failure.
     */
    public static boolean forAll(int[] arr,
            java.util.function.IntPredicate predicate) {
        for (int x : arr) {
            if (!predicate.test(x)) return false;  // found counterexample
        }
        return true;  // no counterexample found
    }

    /**
     * Existential quantifier: ∃x ∈ arr, predicate(x) is true.
     * Java pattern: loop through all, return true on success (witness found).
     */
    public static boolean exists(int[] arr,
            java.util.function.IntPredicate predicate) {
        for (int x : arr) {
            if (predicate.test(x)) return true;  // found witness
        }
        return false;  // no witness found
    }

    /** Find a witness (the actual x) for an existential claim */
    public static java.util.OptionalInt findWitness(int[] arr,
            java.util.function.IntPredicate predicate) {
        for (int x : arr) {
            if (predicate.test(x)) return java.util.OptionalInt.of(x);
        }
        return java.util.OptionalInt.empty();
    }

    public static void main(String[] args) {
        int[] data = {2, 4, 6, 8, 10};

        // ∀x ∈ data, x is even
        System.out.println("All even? " + forAll(data, x -> x % 2 == 0));

        // ∃x ∈ data, x > 7
        System.out.println("Exists > 7? " + exists(data, x -> x > 7));

        // Find witness
        var witness = findWitness(data, x -> x > 7);
        System.out.println("Witness > 7: " + witness);

        // Mixed: ∀x ∈ {1..100}, ∃y ∈ {1..100}, y = 2x  (only for x ≤ 50)
        int[] range = new int[100];
        for (int i = 0; i < 100; i++) range[i] = i + 1;
        boolean result = forAll(range,
            x -> x > 50 || exists(range, y -> y == 2 * x));
        System.out.println("∀x≤50, ∃y=2x in {1..100}: " + result);
    }
}

Example 3: Proof by Contradiction — Combined

Problem: Prove that $\sqrt{2}$ is irrational.

Proof (by contradiction). Assume $\sqrt{2}$ is rational. Then $\sqrt{2} = p/q$ with $p, q \in \mathbb{Z}$, $q \neq 0$, and $\gcd(p, q) = 1$.

Squaring: $2 = p^2/q^2$, so $p^2 = 2q^2$.

Since $p^2$ is even, by Example 1 (contrapositive), $p$ is even. Write $p = 2m$.

Then $4m^2 = 2q^2$, so $q^2 = 2m^2$. By the same argument, $q$ is even.

But then both $p$ and $q$ are even, contradicting $\gcd(p, q) = 1$. $\blacksquare$

Java illustration: We can't prove irrationality in Java, but we can show that $\sqrt{2}$ is not equal to any fraction with a small denominator:

public static void approximateSqrt2() {
    for (int q = 1; q <= 1000; q++) {
        int p = (int) Math.round(q * Math.sqrt(2));
        double approx = (double) p / q;
        double error = Math.abs(approx * approx - 2);
        if (error < 1e-10)
            System.out.printf("  %d/%d ≈ %.10f, error = %.2e%n", p, q, approx, error);
    }
    // None will have error exactly 0 — illustrating irrationality
}

Example 4: Negating Quantified Statements

Problem: Write the negation of: "For all integers $x$, if $x^2$ is even then $x$ is even."

Solution:

Original: $\forall x \in \mathbb{Z},\, (x^2 \text{ is even} \rightarrow x \text{ is even})$

Negation: $\exists x \in \mathbb{Z},\, \neg(x^2 \text{ is even} \rightarrow x \text{ is even})$

Since $\neg(P \rightarrow Q) \equiv P \wedge \neg Q$:

$\exists x \in \mathbb{Z},\, (x^2 \text{ is even} \wedge x \text{ is odd})$

In English: "There exists an integer $x$ such that $x^2$ is even but $x$ is odd."

The original statement is true, so this negation is false — no such $x$ exists.

Example 5: Quantifiers in Specifications

Problem: Express the loop invariant "all elements examined so far are positive" using quantifiers, then implement it as a Java assertion.

Formal statement: After $k$ iterations, $\forall i \in \{0, 1, \ldots, k-1\},\, \text{arr}[i] > 0$.

public static boolean allPositive(int[] arr) {
    for (int k = 0; k < arr.length; k++) {
        // Loop invariant: ∀i ∈ {0,...,k-1}, arr[i] > 0
        // Check the invariant:
        for (int i = 0; i < k; i++) {
            assert arr[i] > 0 : "Invariant violated at i=" + i;
        }
        if (arr[k] <= 0) return false;
    }
    // Postcondition: ∀i ∈ {0,...,n-1}, arr[i] > 0
    return true;
}

Proof Techniques Spotlight

When to Use Each Proof Method

Example decision: "If $3n + 2$ is odd, then $n$ is odd."

• Direct: Assume $3n + 2$ is odd → $3n + 2 = 2k + 1$ → $3n = 2k - 1$ → $n = (2k-1)/3$ → hard to show $n$ is odd.
• Contrapositive: Assume $n$ is even → $n = 2m$ → $3(2m) + 2 = 6m + 2 = 2(3m+1)$ → even. ✓ Much easier!

Java Deep Dive

import java.util.*;
import java.util.function.*;

public class QuantifierLibrary {

    // --- Generic Quantifiers ---

    /** ∀x ∈ collection, predicate(x) */
    public static <T> boolean forAll(Collection<T> items, Predicate<T> pred) {
        for (T item : items) {
            if (!pred.test(item)) return false;
        }
        return true;
    }

    /** ∃x ∈ collection, predicate(x) */
    public static <T> boolean exists(Collection<T> items, Predicate<T> pred) {
        for (T item : items) {
            if (pred.test(item)) return true;
        }
        return false;
    }

    /** Find witness for ∃x, predicate(x) */
    public static <T> Optional<T> findWitness(Collection<T> items, Predicate<T> pred) {
        for (T item : items) {
            if (pred.test(item)) return Optional.of(item);
        }
        return Optional.empty();
    }

    /** Find counterexample for ∀x, predicate(x) — i.e., find x where ¬predicate(x) */
    public static <T> Optional<T> findCounterexample(Collection<T> items, Predicate<T> pred) {
        return findWitness(items, pred.negate());
    }

    // --- Nested Quantifiers ---

    /** ∀x ∈ xs, ∃y ∈ ys, relation(x, y) */
    public static <S, T> boolean forAllExists(Collection<S> xs, Collection<T> ys,
            BiPredicate<S, T> relation) {
        for (S x : xs) {
            boolean found = false;
            for (T y : ys) {
                if (relation.test(x, y)) { found = true; break; }
            }
            if (!found) return false;
        }
        return true;
    }

    /** ∃x ∈ xs, ∀y ∈ ys, relation(x, y) */
    public static <S, T> boolean existsForAll(Collection<S> xs, Collection<T> ys,
            BiPredicate<S, T> relation) {
        for (S x : xs) {
            boolean allTrue = true;
            for (T y : ys) {
                if (!relation.test(x, y)) { allTrue = false; break; }
            }
            if (allTrue) return true;
        }
        return false;
    }

    // --- Proof Methods Demonstrated ---

    /** Direct proof check: if n is even, then n^2 is even */
    public static void demonstrateDirectProof() {
        System.out.println("Direct proof: if n is even, n^2 is even");
        List<Integer> evens = new ArrayList<>();
        for (int n = -100; n <= 100; n += 2) evens.add(n);
        boolean holds = forAll(evens, n -> (n * n) % 2 == 0);
        System.out.println("  Verified for evens in [-100,100]: " + holds);
    }

    /** Contrapositive check: if n^2 is even, then n is even */
    public static void demonstrateContrapositive() {
        System.out.println("Contrapositive: if n is odd, n^2 is odd");
        List<Integer> odds = new ArrayList<>();
        for (int n = -99; n <= 99; n += 2) odds.add(n);
        boolean holds = forAll(odds, n -> (n * n) % 2 != 0);
        System.out.println("  Verified for odds in [-99,99]: " + holds);
    }

    public static void main(String[] args) {
        System.out.println("=== Quantifier Library ===\n");

        List<Integer> numbers = new ArrayList<>();
        for (int i = 1; i <= 20; i++) numbers.add(i);

        // ∀x ∈ {1..20}, x > 0
        System.out.println("All positive: " + forAll(numbers, x -> x > 0));

        // ∃x ∈ {1..20}, x is prime
        System.out.println("Exists prime: " + exists(numbers, QuantifierLibrary::isPrime));

        // Find counterexample: ∀x, x < 15
        System.out.println("Counterexample for all < 15: " +
            findCounterexample(numbers, x -> x < 15));

        // Nested: ∀x ∈ {1..10}, ∃y ∈ {1..10}, x + y = 11
        List<Integer> small = numbers.subList(0, 10);
        System.out.println("∀x, ∃y, x+y=11: " +
            forAllExists(small, small, (x, y) -> x + y == 11));

        System.out.println();
        demonstrateDirectProof();
        demonstrateContrapositive();
    }

    static boolean isPrime(int n) {
        if (n < 2) return false;
        for (int d = 2; d * d <= n; d++) if (n % d == 0) return false;
        return true;
    }
}

Historical Context

Gottlob Frege (1848–1925) invented the formal notation for quantifiers in his Begriffsschrift (1879), creating the first complete system of predicate logic. His notation was different from what we use today but captured the same ideas.

David Hilbert (1862–1943) refined and popularized the $\forall$ and $\exists$ notation and made predicate logic central to his program for formalizing mathematics.

Proof by contradiction dates back to the ancient Greeks. Euclid's proof that there are infinitely many primes (c. 300 BC) is a famous example: assume finitely many primes $p_1, \ldots, p_n$; consider $N = p_1 \cdots p_n + 1$; $N$ is not divisible by any $p_i$, contradiction.

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. State the contrapositive of: "If a function is differentiable, then it is continuous."

A2. Negate: $\forall \epsilon > 0,\, \exists \delta > 0,\, (|x - a| < \delta \rightarrow |f(x) - L| < \epsilon)$.

A3. Which Java loop pattern corresponds to $\forall$? Which to $\exists$?

A4. True or false: "If $P \rightarrow Q$ is true and $Q$ is true, then $P$ must be true."

Slide Set B: Proof Problems

B1. Prove by contrapositive: If $3n + 2$ is odd, then $n$ is odd.

B2. Prove by contradiction: There is no largest prime number.

B3. Negate and simplify: "For all arrays $A$, if $A$ is sorted, then binary search on $A$ returns the correct result."

Slide Set C: Java Coding Problems

C1. Write boolean forAll(int[] arr, IntPredicate p) and boolean exists(int[] arr, IntPredicate p).

C2. Write a method that finds a counterexample to a universal claim over {1,...,1000}.

C3. Express the loop invariant "the current maximum is at least as large as all elements seen so far" using forAll, and check it at each iteration.

Full Problem Set

Discrete Math Problems

DM1. For each statement, write its converse, inverse, and contrapositive:

(a) If $n$ is prime, then $n$ is odd or $n = 2$.

(b) If $a \mid b$ and $b \mid c$, then $a \mid c$.

DM2. Prove by contrapositive: If $n^3$ is odd, then $n$ is odd.

DM3. Prove by contradiction: $\sqrt{3}$ is irrational.

DM4. Negate each statement and determine whether the original or its negation is true:

(a) $\forall n \in \mathbb{Z},\, n^2 \geq 0$.

(b) $\exists n \in \mathbb{Z},\, n^2 + n + 1 = 0$.

(c) $\forall n \in \mathbb{N},\, \exists m \in \mathbb{N},\, m > n$.

DM5. Prove: For all integers $a$ and $b$, if $a + b \geq 15$, then $a \geq 8$ or $b \geq 8$.

DM6. Let $P(x, y)$ mean "$x + y$ is even." Determine the truth values of:

(a) $\forall x \in \mathbb{Z},\, P(x, x)$.

(b) $\forall x \in \mathbb{Z},\, \exists y \in \mathbb{Z},\, P(x, y)$.

(c) $\exists x \in \mathbb{Z},\, \forall y \in \mathbb{Z},\, P(x, y)$.

DM7. Prove or disprove: For all positive integers $n$, $2^n > n^2$.

Java Programming Problems

JP1. Write a method <T> Optional<T> findCounterexample(Iterable<T> domain, Predicate<T> claim) that finds an element violating the claim.

JP2. Implement nested quantifier evaluation: forAllExists(IntStream xs, IntStream ys, BiPredicate<Integer,Integer> p).

JP3. Write a method that takes two arrays and checks: $\forall i,\, \text{arr1}[i] \leq \text{arr2}[i]$ (element-wise comparison).

JP4. Implement a method that checks whether a relation (given as a Set<int[]> of pairs) is: reflexive, symmetric, transitive, antisymmetric.

JP5. Write a precondition checker: given a method that requires "arr is sorted", write boolean isSorted(int[] arr) expressed using a universal quantifier: $\forall i \in \{0, \ldots, n-2\},\, \text{arr}[i] \leq \text{arr}[i+1]$.

JP6. Write a Java method that empirically tests "for all even $n$ in [4, 10000], $n$ is the sum of two primes" (Goldbach's conjecture). Find a witness pair for each.

Bridge Problems

BR1. The claim "binary search returns the correct index" can be formalized as: $\forall \text{sorted arrays } A,\, \forall k,\, (\text{binarySearch}(A, k) = i \rightarrow A[i] = k)$. Negate this claim and write Java code that searches for a counterexample.

BR2. Prove by contradiction that any comparison-based sorting algorithm requires $\Omega(n \log n)$ comparisons in the worst case. (Hint: there are $n!$ possible permutations; each comparison splits the possibilities in at most two.) Then write a Java program that counts comparisons in your implementation of merge sort and verifies the lower bound empirically.

BR3. Express the following using quantifiers and implement each as a Java method:

(a) "Array contains a duplicate" — $\exists i,\, \exists j,\, i \neq j \wedge \text{arr}[i] = \text{arr}[j]$.

(b) "Array is a permutation of {1,...,n}" — $\forall k \in \{1,\ldots,n\},\, \exists i,\, \text{arr}[i] = k$.

Solutions

Discrete Math Solutions

DM1a. Original: If $n$ prime → $n$ odd or $n=2$. Converse: If $n$ odd or $n=2$ → $n$ prime (false: 9 is odd but not prime). Inverse: If $n$ not prime → $n$ not odd and $n \neq 2$ (false: 9). Contrapositive: If $n$ not odd and $n \neq 2$ → $n$ not prime (true: even numbers > 2 are not prime).

DM2. Contrapositive: if $n$ is even, then $n^3$ is even. Let $n = 2k$. Then $n^3 = 8k^3 = 2(4k^3)$, which is even. $\blacksquare$

DM3. Assume $\sqrt{3} = p/q$ with $\gcd(p,q) = 1$. Then $3q^2 = p^2$, so $3 \mid p^2$, so $3 \mid p$ (since 3 is prime). Write $p = 3m$. Then $3q^2 = 9m^2$, so $q^2 = 3m^2$, so $3 \mid q$. But then $3 \mid \gcd(p,q)$, contradicting $\gcd(p,q) = 1$. $\blacksquare$

DM4. (a) Negation: $\exists n, n^2 < 0$. Original is true (squares are non-negative). (b) Negation: $\forall n, n^2 + n + 1 \neq 0$. The discriminant $1 - 4 = -3 < 0$, so no integer solutions. Negation is true, original is false. (c) Negation: $\exists n, \forall m, m \leq n$. This says natural numbers are bounded. Original is true (no largest natural number).

DM5. By contrapositive: if $a < 8$ and $b < 8$, then $a + b < 16$. Since $a \leq 7$ and $b \leq 7$, $a + b \leq 14 < 15$. $\blacksquare$

DM6. (a) True: $x + x = 2x$ is always even. (b) True: take $y = x$ (or any $y$ with same parity as $x$). (c) True: take $x = 0$ (even); $0 + y$ is even iff $y$ is even — wait, that's not for all $y$. Take $x = 2$; $2 + 1 = 3$ is odd. So (c) is false: no single $x$ makes $x + y$ even for all $y$.

DM7. False for small $n$: $2^1 = 2 > 1 = 1^2$ ✓, $2^2 = 4 = 4 = 2^2$ NO (not strictly greater). $2^3 = 8 < 9 = 3^2$ ✗. Counterexample: $n = 3$.

Java Solutions

JP4.

public static boolean isReflexive(Set<int[]> rel, Set<Integer> domain) {
    return forAll(domain, a ->
        exists(rel, pair -> pair[0] == a && pair[1] == a));
}

public static boolean isSymmetric(Set<int[]> rel) {
    return forAll(rel, pair ->
        exists(rel, p2 -> p2[0] == pair[1] && p2[1] == pair[0]));
}

public static boolean isTransitive(Set<int[]> rel) {
    return forAll(rel, ab ->
        forAll(rel, bc ->
            ab[1] != bc[0] || exists(rel, ac ->
                ac[0] == ab[0] && ac[1] == bc[1])));
}

JP5.

public static boolean isSorted(int[] arr) {
    // ∀i ∈ {0,...,n-2}, arr[i] <= arr[i+1]
    for (int i = 0; i < arr.length - 1; i++) {
        if (arr[i] > arr[i + 1]) return false;  // counterexample found
    }
    return true;
}

JP6.

public static void testGoldbach(int limit) {
    boolean[] sieve = new boolean[limit + 1];
    Arrays.fill(sieve, true);
    sieve[0] = sieve[1] = false;
    for (int p = 2; p * p <= limit; p++)
        if (sieve[p]) for (int j = p*p; j <= limit; j += p) sieve[j] = false;

    for (int n = 4; n <= limit; n += 2) {
        boolean found = false;
        for (int p = 2; p <= n / 2; p++) {
            if (sieve[p] && sieve[n - p]) {
                System.out.printf("  %d = %d + %d%n", n, p, n - p);
                found = true;
                break;
            }
        }
        assert found : "Goldbach failed for " + n;
    }
}

Learning Objectives

• Apply inference rules (modus ponens, modus tollens) to reason about program behavior.
• Use assert statements to encode preconditions and postconditions.
• Annotate methods with @requires and @ensures comments.
• Reason about program correctness using Hoare-style triples {P} C {Q}.
• Combine assertions with logical reasoning to debug and verify programs.

Concept Overview

Inference Rules

Modus Ponens: If $P$ is true and $P \rightarrow Q$ is true, then $Q$ is true.

Modus Tollens: If $\neg Q$ is true and $P \rightarrow Q$ is true, then $\neg P$ is true.

Hypothetical Syllogism: If $P \rightarrow Q$ and $Q \rightarrow R$, then $P \rightarrow R$.

Predicates and Assertions

A predicate is a Boolean-valued function: $P(x)$ returns true or false depending on $x$. In Java, this is a method returning boolean or a Predicate<T>.

An assertion is a predicate that we expect to be true at a specific point in the program:

assert condition : "error message";

If condition is false and assertions are enabled (-ea), the program throws AssertionError.

Hoare Triples (Informal)

A Hoare triple $\{P\}\ C\ \{Q\}$ means: "If precondition $P$ holds before executing code $C$, and $C$ terminates, then postcondition $Q$ holds after."

Example: $\{\text{arr is sorted}\}\ \text{binarySearch(arr, key)}\ \{\text{returns correct index or -1}\}$

Why this matters in CS:

• Design by Contract: Methods have preconditions (what the caller guarantees) and postconditions (what the method guarantees).
• Debugging: Assertions catch bugs early by checking expected conditions at runtime.
• Verification: Formal reasoning about program correctness uses Hoare logic.
• Documentation: @requires and @ensures comments serve as executable documentation.

Formal Notation

Worked Examples

Example 1: Modus Ponens in Code — Discrete Math + Java

Problem: A method specifies: "If the input array is sorted, then the output is the correct index of the key." The caller verifies the array is sorted. Conclude the output is correct.

Formal reasoning:

• $P$: array is sorted (verified by caller)
• $P \rightarrow Q$: method specification
• By modus ponens, $Q$: output is correct.

/**
 * @requires arr is sorted in non-decreasing order
 * @ensures returns index i where arr[i] == key, or -1 if not found
 */
public static int binarySearch(int[] arr, int key) {
    assert isSorted(arr) : "Precondition violated: array not sorted";

    int lo = 0, hi = arr.length - 1;
    while (lo <= hi) {
        int mid = lo + (hi - lo) / 2;  // avoid overflow
        if (arr[mid] == key) return mid;
        else if (arr[mid] < key) lo = mid + 1;
        else hi = mid - 1;
    }
    return -1;
}

private static boolean isSorted(int[] arr) {
    for (int i = 0; i < arr.length - 1; i++) {
        if (arr[i] > arr[i + 1]) return false;
    }
    return true;
}

Example 2: Modus Tollens for Debugging

Problem: A method's postcondition guarantees "the returned value is non-negative." The caller observes a negative return value. Conclude the precondition was violated.

Formal reasoning:

• Specification: $P \rightarrow Q$ where $Q$ is "return ≥ 0"
• Observed: $\neg Q$ (return < 0)
• By modus tollens: $\neg P$ (precondition violated)

/**
 * @requires n >= 0
 * @ensures result >= 0 and result * result <= n < (result + 1) * (result + 1)
 */
public static int intSqrt(int n) {
    assert n >= 0 : "Precondition: n must be non-negative";
    int r = (int) Math.sqrt(n);
    // Postcondition check
    assert r >= 0 : "Postcondition: result must be non-negative";
    assert (long) r * r <= n : "Postcondition: r*r <= n";
    assert (long) (r + 1) * (r + 1) > n : "Postcondition: (r+1)^2 > n";
    return r;
}

Example 3: Hoare Triple for Assignment — Combined

Problem: Prove $\{x = 5\}\ y = x + 3\ \{y = 8\}$.

Proof. Given: $x = 5$ (precondition). After executing $y = x + 3$: $y = 5 + 3 = 8$. So postcondition $y = 8$ holds. $\blacksquare$

Hoare's assignment axiom: $\{Q[x/E]\}\ x = E\ \{Q\}$.

To establish $\{?\}\ y = x + 3\ \{y = 8\}$: substitute $y$ with $x + 3$ in postcondition: $x + 3 = 8$, i.e., $x = 5$. ✓

public static void demonstrateHoareAssignment() {
    int x = 5;
    assert x == 5;     // Precondition
    int y = x + 3;
    assert y == 8;     // Postcondition
    System.out.println("Hoare triple verified: {x=5} y=x+3 {y=8}");
}

Example 4: Sequential Composition

Problem: Prove $\{x = 3\}\ x = x + 1;\ y = x * 2\ \{y = 8\}$.

Proof. After $x = x + 1$: $x = 4$. After $y = x \times 2$: $y = 8$. $\blacksquare$

Using the composition rule: find a midcondition $R$ such that $\{P\}\ C_1\ \{R\}$ and $\{R\}\ C_2\ \{Q\}$.

• $\{x = 3\}\ x = x+1\ \{x = 4\}$
• $\{x = 4\}\ y = x*2\ \{y = 8\}$

Example 5: Conditional Reasoning

Problem: Verify the correctness of max(a, b):

/**
 * @requires true (no precondition)
 * @ensures result >= a && result >= b && (result == a || result == b)
 */
public static int max(int a, int b) {
    int result;
    if (a >= b) {
        // Here: a >= b
        result = a;
        // Here: result >= a && result >= b && result == a
    } else {
        // Here: a < b, so b > a
        result = b;
        // Here: result >= a && result >= b && result == b
    }
    // In both cases: result >= a && result >= b && (result == a || result == b)
    assert result >= a && result >= b;
    assert result == a || result == b;
    return result;
}

Proof Techniques Spotlight

Reasoning About Code with Logic

The key insight: every line of code transforms a logical state.

Template for method verification:

1. State precondition $P$.
2. For each statement, compute the resulting condition.
3. At the end, show the postcondition $Q$ follows from the final condition.

Java Deep Dive

import java.util.*;

public class ProgramReasoningLibrary {

    // --- Design by Contract ---

    /**
     * Binary search with full contract.
     * @requires arr != null && arr is sorted (non-decreasing)
     * @ensures result == -1 implies key not in arr
     *          result >= 0 implies arr[result] == key
     */
    public static int binarySearch(int[] arr, int key) {
        // Check precondition
        assert arr != null : "Precondition: arr must not be null";
        assert isSorted(arr) : "Precondition: arr must be sorted";

        int lo = 0, hi = arr.length - 1;

        // Loop invariant: if key is in arr, then key is in arr[lo..hi]
        while (lo <= hi) {
            // Invariant check
            assert lo >= 0 && hi < arr.length;

            int mid = lo + (hi - lo) / 2;
            if (arr[mid] == key) {
                assert arr[mid] == key;  // postcondition for found case
                return mid;
            }
            if (arr[mid] < key) {
                lo = mid + 1;
            } else {
                hi = mid - 1;
            }
        }

        // Loop terminated: lo > hi
        // By invariant and loop exit: key is not in arr
        return -1;
    }

    /**
     * Selection sort with invariant annotations.
     * @requires arr != null
     * @ensures arr is sorted and arr is a permutation of original arr
     */
    public static void selectionSort(int[] arr) {
        assert arr != null;

        for (int i = 0; i < arr.length - 1; i++) {
            // Invariant: arr[0..i-1] is sorted and contains
            //            the i smallest elements of the original array

            // Find minimum in arr[i..n-1]
            int minIdx = i;
            for (int j = i + 1; j < arr.length; j++) {
                if (arr[j] < arr[minIdx]) minIdx = j;
            }

            // Swap arr[i] and arr[minIdx]
            int temp = arr[i]; arr[i] = arr[minIdx]; arr[minIdx] = temp;

            // After swap: arr[0..i] is sorted and contains the i+1 smallest elements
            assert isSorted(arr, 0, i + 1) : "Invariant broken at i=" + i;
        }

        // Postcondition: arr is fully sorted
        assert isSorted(arr) : "Postcondition: arr should be sorted";
    }

    /**
     * Safe division with precondition.
     * @requires divisor != 0
     * @ensures result * divisor == dividend (for exact division)
     */
    public static int safeDivide(int dividend, int divisor) {
        if (divisor == 0) throw new ArithmeticException("Division by zero");
        return dividend / divisor;
    }

    /**
     * Array maximum with full reasoning.
     * @requires arr != null && arr.length >= 1
     * @ensures result >= arr[i] for all i, and result == arr[j] for some j
     */
    public static int max(int[] arr) {
        assert arr != null && arr.length >= 1 : "Precondition: non-empty array";

        int result = arr[0];
        // Invariant: result = max(arr[0..0])

        for (int i = 1; i < arr.length; i++) {
            // Invariant: result = max(arr[0..i-1])
            if (arr[i] > result) {
                result = arr[i];
            }
            // Invariant maintained: result = max(arr[0..i])
        }

        // Postcondition: result = max(arr[0..n-1])
        return result;
    }

    // --- Helper Methods ---

    static boolean isSorted(int[] arr) {
        return isSorted(arr, 0, arr.length);
    }

    static boolean isSorted(int[] arr, int from, int to) {
        for (int i = from; i < to - 1; i++) {
            if (arr[i] > arr[i + 1]) return false;
        }
        return true;
    }

    // --- Demonstration ---

    public static void main(String[] args) {
        System.out.println("=== Program Reasoning Library ===\n");

        // Binary search with contract
        int[] sorted = {2, 5, 8, 12, 16, 23, 38, 56, 72, 91};
        System.out.println("Search for 23: index " + binarySearch(sorted, 23));
        System.out.println("Search for 50: index " + binarySearch(sorted, 50));

        // Selection sort with invariants
        int[] unsorted = {64, 25, 12, 22, 11};
        System.out.println("\nBefore sort: " + Arrays.toString(unsorted));
        selectionSort(unsorted);
        System.out.println("After sort:  " + Arrays.toString(unsorted));

        // Max with postcondition verification
        int[] data = {3, 7, 2, 9, 4, 6, 1};
        int m = max(data);
        System.out.println("\nMax of " + Arrays.toString(data) + " = " + m);

        // Verify postcondition explicitly
        boolean atLeastAsLarge = true, existsEqual = false;
        for (int x : data) {
            if (m < x) atLeastAsLarge = false;
            if (m == x) existsEqual = true;
        }
        System.out.println("Postcondition (>= all): " + atLeastAsLarge);
        System.out.println("Postcondition (in arr): " + existsEqual);
    }
}

Historical Context

C.A.R. Hoare published "An Axiomatic Basis for Computer Programming" in 1969, introducing what we now call Hoare logic. His notation $\{P\}\ C\ \{Q\}$ gave programmers a mathematical framework for proving programs correct.

Edsger Dijkstra extended this work with weakest precondition calculus in his 1976 book A Discipline of Programming. Given a postcondition $Q$ and a program $C$, the weakest precondition $\text{wp}(C, Q)$ is the weakest condition that guarantees $Q$ after executing $C$.

Bertrand Meyer popularized Design by Contract in the 1980s with the Eiffel programming language, which had built-in support for preconditions, postconditions, and class invariants. Java's assert keyword (added in Java 1.4) provides a lighter-weight version of this concept.

Modern verification tools like JML (Java Modeling Language), Dafny, Coq, and Isabelle allow machine-checked proofs of program correctness.

Slide-Ready Problem Sets

Slide Set A: Conceptual Questions

A1. In the Hoare triple $\{x > 0\}\ y = x * 2\ \{y > 0\}$, what is the precondition? The postcondition?

A2. A method's postcondition says "return value ≥ 0." You observe a return of -3. What can you conclude?

A3. What does assert false do? When would you use it?

A4. Explain the difference between partial correctness and total correctness.

Slide Set B: Proof Problems

B1. Prove $\{x = 10\}\ x = x - 3\ \{x = 7\}$ using the assignment axiom.

B2. Prove $\{a \geq 0 \wedge b \geq 0\}\ c = a + b\ \{c \geq 0\}$.

B3. Write the Hoare triple for int max = (a > b) ? a : b; and prove it correct.

Slide Set C: Java Coding Problems

C1. Annotate a linearSearch method with @requires and @ensures comments, then add assert statements.

C2. Write a method insertSorted(int[] arr, int len, int key) that inserts into a sorted array, and annotate with invariants.

C3. Add postcondition assertions to a swap(int[] arr, int i, int j) method.

Full Problem Set

Discrete Math Problems

DM1. Using modus ponens, derive a conclusion from: (1) "If it rains, the ground is wet." (2) "It is raining."

DM2. Using modus tollens, derive a conclusion from: (1) "If the program has no bugs, all tests pass." (2) "Test 3 failed."

DM3. From the premises: $P \rightarrow Q$, $Q \rightarrow R$, $P$, derive $R$ using inference rules. Name each step.

DM4. Prove using logical reasoning: if a method satisfies $\{P\}\ C_1\ \{R\}$ and $\{R\}\ C_2\ \{Q\}$, then $\{P\}\ C_1; C_2\ \{Q\}$ (composition rule).

DM5. Is the following argument valid? "If $n$ is prime, then $n$ is odd or $n = 2$. $n$ is even and $n \neq 2$. Therefore $n$ is not prime." Formalize and check.

DM6. Prove: If a function satisfies $\{\text{true}\}\ f()\ \{Q\}$, then $Q$ holds unconditionally after $f$ terminates (regardless of inputs).

DM7. Explain why $\{\text{false}\}\ C\ \{Q\}$ is trivially true for any $C$ and $Q$.

Java Programming Problems

JP1. Write a method int linearSearch(int[] arr, int key) with @requires, @ensures, and assertions for both the found and not-found cases.

JP2. Write void insertionSort(int[] arr) with a loop invariant: "after iteration $i$, arr[0..i] is sorted." Verify the invariant with assertions.

JP3. Write a Stack class with push, pop, peek, isEmpty methods. Add preconditions (e.g., pop requires !isEmpty()) and postconditions using assertions.

JP4. Write a method that computes the GCD and annotates every step with the loop invariant: "gcd(original\_a, original\_b) = gcd(current\_a, current\_b)". Verify at each iteration.

JP5. Implement a BankAccount class with deposit(amount) and withdraw(amount). Add preconditions (positive amounts, sufficient balance) and postconditions (balance updated correctly). Use assertions.

JP6. Write a method int[] merge(int[] a, int[] b) that merges two sorted arrays into one sorted array. Annotate with invariants and verify postcondition (result is sorted and has correct length).

Bridge Problems

BR1. Take the binary search code from Example 1. Formally state the loop invariant, prove initialization (it holds before the loop), maintenance (it is preserved by each iteration), and termination (when the loop exits, the postcondition follows).

BR2. Write a Java method that implements Euclid's algorithm and at every iteration prints: (a) the current values of $a, b$, (b) the loop invariant ("gcd(a,b) = gcd(original\_a, original\_b)"), and (c) the variant function value ($b$). Verify all three.

BR3. Implement a method boolean containsPrime(int[] arr) with specification: "returns true if and only if arr contains at least one prime number." Use modus ponens to argue: if the array {4, 6, 7, 8} is passed, the method returns true (because 7 is prime, and the specification guarantees correct behavior).

Solutions

Discrete Math Solutions

DM1. Premises: $P$ ("raining") and $P \rightarrow Q$ ("raining → ground wet"). By modus ponens: $Q$ ("ground is wet"). $\blacksquare$

DM2. Premises: $P \rightarrow Q$ ("no bugs → all tests pass") and $\neg Q$ ("test 3 failed" → "not all tests pass"). By modus tollens: $\neg P$ ("the program has bugs"). $\blacksquare$

DM3. 1. $P$ (given). 2. $P \rightarrow Q$ (given). 3. $Q$ (modus ponens from 1, 2). 4. $Q \rightarrow R$ (given). 5. $R$ (modus ponens from 3, 4). $\blacksquare$

DM5. Formalize: $P$: "$n$ is prime." $Q$: "$n$ is odd or $n = 2$." Premise 1: $P \rightarrow Q$. Premise 2: $\neg Q$ (i.e., "$n$ is even and $n \neq 2$", which means $\neg(n \text{ odd or } n = 2)$). By modus tollens: $\neg P$. The argument is valid. $\blacksquare$

DM7. $\{\text{false}\}\ C\ \{Q\}$ says "if false holds before $C$, then $Q$ holds after." Since the precondition is never satisfied (false is never true), the triple is vacuously true. $\blacksquare$

Java Solutions

JP1.

/**
 * @requires arr != null
 * @ensures returns i >= 0 with arr[i] == key, or -1 if key not in arr
 */
public static int linearSearch(int[] arr, int key) {
    assert arr != null : "Precondition: arr must not be null";
    for (int i = 0; i < arr.length; i++) {
        // Invariant: key not in arr[0..i-1]
        if (arr[i] == key) {
            assert arr[i] == key;  // postcondition for found case
            return i;
        }
    }
    // Postcondition for not-found: key not in arr[0..n-1]
    return -1;
}

JP2.

public static void insertionSort(int[] arr) {
    for (int i = 1; i < arr.length; i++) {
        // Invariant: arr[0..i-1] is sorted
        assert isSorted(arr, 0, i);
        int key = arr[i];
        int j = i - 1;
        while (j >= 0 && arr[j] > key) {
            arr[j + 1] = arr[j];
            j--;
        }
        arr[j + 1] = key;
        // Invariant maintained: arr[0..i] is sorted
        assert isSorted(arr, 0, i + 1);
    }
    assert isSorted(arr);
}

JP4.

public static int gcdWithInvariant(int a, int b) {
    int origA = a, origB = b;
    while (b != 0) {
        // Invariant: gcd(a, b) == gcd(origA, origB)
        assert gcd(a, b) == gcd(origA, origB)
            : "Invariant failed: gcd(" + a + "," + b + ")";
        // Variant: b (strictly decreasing, non-negative)
        int oldB = b;
        int r = a % b;
        a = b;
        b = r;
        assert b < oldB : "Variant not decreasing";
    }
    assert a == gcd(origA, origB) : "Postcondition failed";
    return a;
}

JP6.

/**
 * @requires a is sorted, b is sorted
 * @ensures result is sorted and result.length == a.length + b.length
 */
public static int[] merge(int[] a, int[] b) {
    assert isSorted(a) && isSorted(b);
    int[] result = new int[a.length + b.length];
    int i = 0, j = 0, k = 0;
    while (i < a.length && j < b.length) {
        // Invariant: result[0..k-1] is sorted, contains a[0..i-1] and b[0..j-1]
        if (a[i] <= b[j]) result[k++] = a[i++];
        else result[k++] = b[j++];
    }
    while (i < a.length) result[k++] = a[i++];
    while (j < b.length) result[k++] = b[j++];
    assert isSorted(result);
    assert result.length == a.length + b.length;
    return result;
}