• Propositional Logic:
  • A proposition is a statement that is either true or false
  • Propositions can be combined into expressions/sentences using logical operators/connectives
  • The resulting expressions/sentences are either true or false
• Predicate Logic:
  • A predicate is a function that has a range of {T,F}
  • Predicates can be combined into expressions/sentences using logical operators/connectives
  • Sentences can also be formed using quantifiers
  • Propositional functions can be made a proposition by assigning variables to all variables (i.e., by binding all variables) or using quantification

• Use predicate logic to prove that code fragments are correct
• Combine all of the code fragment correctness proofs to show that a program is correct

• Pre-Condition:
  • A predicate that describes the initial state (i.e., before the code fragment is executed)
• Post-Condition:
  • A predicate that describes the final/terminal state (i.e., before the code fragment is executed)

• The Guard:
  • The predicate that determines whether the body of the loop should be entered
  • Often denoted by \(G\)
• The Invariant:
  • A predicate that is true when control enters a loop, remains true each time the body of the loop finishes executing, and is still true when control exits the loop
  • Often denoted by \(I\)

• Defined:
  • If the pre-conditions are true and the loop is executed then the post-conditions are true
• Proofs of Correctness:
  • Are inductive

Given a while loop with guard \(G\), pre-conditions, post-conditions, and a predicate \(I(k)\) describing the loop invariant at iteration \(k\), the loop is correct if the following hold:

1. \(I(0)\) is true. (Basis Property)
2. If \(G\) is true and \(I(k)\) is true then \(I(k+1)\) is true. (Inductive Property)
3. \(G\) becomes false after a finite number of iterations. (Eventual Falsity of the Guard)
4. Letting \(n\) denote the smallest number of iterations after which \(G\) is false, if \(I(n)\) is true then the post-conditions are true. (Correctness of the Post-Conditions)

• Pre-Conditions:
  • \(a \geq 0\) and integer (Input)
  • \(d \gt 0\) and integer (Input)
  • \(r = a\)
  • \(q = 0\)
• Loop:
  • while \((r \geq d)\)
    {
  • \(r - = d;\)
  • \(++q;\)
  • }
• Post-Conditions:
  • \(a = q * d + r\)
  • \(0 \leq r\)
  • \(r \lt d\)

• Pre-Conditions:
  • \(m \geq 0\) and integer (Input)
  • \(x \gt 0\) and integer (Input)
  • \(k = 0\)
  • \(p = 0\)
• Loop:
  • while \((k \lt m)\)
    {
  • \(p + = x;\)
  • \(++k;\)
  • }
• Post-Conditions:
  • \(p = m * x\)

• The Guard:
  • \(G(k,m) \doteq (k \lt m)\)
• A Loop Invariant:
  • \(I(k) \doteq (k = n) \wedge (p = n x) \)

Basis Property:

1. \(k = 0\) is true
2. \(p = k x\) is true because \(0 = 0 x\) is true for all \(x\)

Inductive Property:

Suppose that before iteration \(k\) of the loop the guard is true (i.e., \(k \lt m\) is true) and \(I(k)\) is true (i.e., \(k = n\) is true and \(p = n x\) is true).

We must show that after the iteration, \(I(k+1)\) is true.

1. \(p_{k+1} = p_{k} + x = k x + x = (k + 1) x\) is true
2. \(k + 1 = k + 1\) is true
3. So \(I(k+1)\) is true

Eventual Falsity of the Guard:

1. \(k = m\) is true
2. So the guard is true after \(m\) iterations

Correctness of the Post Condition:

1. \(G\) becomes false after \(m\) iterations
2. So \(m = k = n\) is true and \(p = m x\) is true

• The Problem:
  • Given \(s \in \mathbb{Z}_{++}\), find the largest integer \(r \in \mathbb{Z}_{++}\) such that \(r \leq \sqrt{s}\) is true
• Pre-Conditions:
  • \(s \gt 0\) and integer (Input)
  • \(r = 1\)
• One Algorithm:
  • while \((r^{2} \leq s)\)
    {
  • \(++r;\)
  • }
    \(--r;\)
• What Post-Conditions Hold?
  \((r+1)^{2} \gt s\)
  \(r^{2} \leq s\)
• Is This Algorithm Correct?
  How should we check?

unsigned int floorsqrt(unsigned long x)
{
    unsigned long r, nr, m;
 
    r = 0;
    m = 0x40000000;
    do 
    {
        nr = r + m;
        if (nr <= x) 
        {
            x -= nr;
            r = nr + m;
        }
        r >>= 1;
        m >>= 2;

    } while (m != 0);
 
    return(r);
}

• Question:
  • Which (correct) algorithm is better?
• Answer:
  • That's a different topic completely

• The Problem:
  • Given \(b \in \mathbb{Z}_{+}\) and \(a \in \mathbb{Z}_{++}\), find the greatest common divisor of \(a\) and \(b\)
• Pre-Conditions:
  • \(b_{0} \geq 0\)
  • \(a_{0} \gt b_{0}\)
  • \(r = b_{0}\)
• Loop:
  • while \((b_k \gt 0)\)
    {
  • \(r_{k+1} \doteq a_{k} \mod b_{k};\)
  • \(a_{k+1} \doteq b_{k};\)
  • \(b_{k+1} \doteq r_{k+1};\)
  • }
• Post-Conditions:
  • \(a_{n} = \gcd(a_{0}, b_{0})\)

• Preliminary Lemma:
  • If \(r = 1 \mod b\) then \(\gcd(a,b) = \gcd(b,r)\) is true
• A Loop Invariant:
  • \(I(k) \doteq (\gcd(a_k ,b_k) = \gcd(a_0, b_0)) \wedge (b_k \geq 0) \wedge (a_k \gt b_k) \)

Basis Property:

1. \(I(0) \doteq (\gcd(a_0 ,b_0) = \gcd(a_0, b_0)) \wedge (b_0 \geq 0) \wedge (a_0 \gt b_0)\) is true

Inductive Property:

Suppose that before iteration \(k\) of the loop the guard is true (i.e., \(b_k \gt 0\) is true) and \(I(k)\) is true [i.e., \(\gcd(a_k , b_k) = \gcd(a_0 , b_0)\) is true and \(b_k \geq 0\) is true and \(a_k \gt b_k\) is true].

We must show that after the iteration, \(I(k+1)\) is true (i.e., \(\gcd(a_{k+1},b_{k+1}) = \gcd(a_0 , b_0)\) is true and \(b_{k+1} \geq 0\) is true and \(a_{k+1} \gt b_{k+1}\) is true).

1. \(a_{k+1} = b_{k}\) is true
2. \(b_{k+1} = r_{k+1} = a_{k} \mod b_{k}\) is true
3. \(\gcd(a_{k+1}, b_{k+1}) = \gcd(b_{k}, b_{k+1})\) is true
4. \(= \gcd(b_{k}, a_{k})\) is true (from the lemma)
5. \(= \gcd(a_{0},b_{0})\) is true (because \(I(k)\) is true)
6. \(b_{k+1} \geq 0\) is true
7. \(a_{k+1} \gt b_{k+1}\) is true
8. So \(I(k+1)\) is true

Eventual Falsity of the Guard:

1. \(b\) is an integer
2. Each iteration of the loop reduces \(b\)
3. \(b\) is non-negative (from the loop invariant)
4. So, \(b\) will eventually be 0

Correctness of the Post Condition:

1. Suppose that for some integer \(n\), the guard, \(G\) is false (in which case \(b = 0\) is true) and \(I(n)\) is true (i.e., \(\gcd(a_{n},b_{n}) = \gcd(a_{0},b_{0})\) is true and \(b_{n} = 0\) is true and \(a_{n} \gt b_{n}\) is true
2. It follows that \(\gcd(a_{0},b_{0}) = \gcd(a_{n},b_{n}) = \gcd(a_{n},0) = a_{n}\) is true so the post-condition is true