Theory Applied
First Order Logic in Processor Specifications
After the floating-point error was discovered in the Pentium chip, Intel began to research formal verification in order to avoid other embarassing bugs. To make the lessons of the Theory section more relevant, here is an example from Intel's formal verification research.
The following describes the processor's behavior in response to numbers approaching negative infinity:
"When rounding towards negative infinity, the result shall be the format's value ... closest to and no greater than the infinitely precise result."
|
Formal specification: round(toNegInf, R, V) = (R <= V) ^ (V < R + ulp+) Read <= as 'less than or equal to,' not as a left arrow. Let R = rounded result, V = value to be rounded, and ulp+ = the smallest representable increment. |
Algorithms as used in Theorem Provers
Boyer-Moore Induction [cit]
Boyer and Moore illustrated their automated theorem proving algorithm, including their heuristic (method of helping the machine guess), by proving the associative property of multiplication.
Their theorem prover uses the concept of induction. To prove that a theorem is true by induction, you must show two things. 1) Base case- Show that it is true for x = 0. 2) Inductive case - Assuming that the theorem is true for x = k, show that it is also true for x = k + 1.
Prove: (x*y)*z = x*(y*z) (IH)
The machine is armed with the following definitions (s(x) is the successor of x, x+1):
0 + y = y; s(x) + y = s(x+y)
0 * y = 0; s(x) * y = y + (x*y)
Base Case:
(0*y) * z = 0 * (y*z) -----> 0 = 0 True!
Induction Case:
(s(x) * y) * z = s(x) * (y * z) (1)
By definition, (y + x * y) * z = (y * z) + (x * (y * z)).(2)
Since further exapnding the previous statement would introduce terms not already in the conjecture at this point, the program stops expanding at this point.
Next, the program attempts to use the induction hypothesis (IH). The right hand side of the induction hypothesis (x*y)*z = x*(y*z) has "stepped-through" the proof, showing up on the right side of (2). Therefore:
(y + x * y) * z = (y * z) + ((x * y) * z) (3)
Although the program's goal is to prove that (IH) implies (3), the program uses the technique of generalization by adopting the stronger goal of proving that (3) is true in general, regardless of (IH). Also, since (x*y) has "stepped-through" on both sides of (3), the program generalizes further by letting w = x * y and proving:
(y + w) * z = (y * z) + (w * z) (4).
Here, in (4), we have stumbled upon the distributive property of multiplication. The program then proves this using the same processes of induction described above. This proof, performed in the early 1980s, took 10 seconds to perform on a DEC 2060 in Interlisp.