# Class 03: Program Verification

Back to Binary Search. On to The Structure of a Computer.

Held: Wednesday, 22 January 2003

Summary: Today we begin our consideration of why one might want to formally verify algorithms and programs and the tools one uses to do so.

Assignments:

Due

Notes:

• I plan to read your introductory surveys tomorrow and respond by Friday.
• I'm still playing with the syllabus, and will be for a little while.
• Sorry about forgetting to include a Homework 1 entry in the ECA. That's fixed now.

## Verification, Revisited

• As we noted yesterday, programmers who are fairly sure that they've implemented a program correctly can be wrong.
• Testing reveals some errors.
• Methodical testing reveals even more.
• However, testing should be coupled with some careful analysis.
• Ideally, the analysis would precede and guide the implementation.
• Gries's book provides a useful mechanism for the analysis and design of algorithms and programs.
• How will we approach this mechanism?
• We'll start with some background in symbolic logic, some of which you'll find is mostly review of things you've learned informally.
• This week: Basics of Boolean logic.
• Next week: Basics of Boolean reasoning.
• Week three: Predicates and quantifiers.
• Week five: Assertions about arrays.
• Week six: Using assertions in documentation.
• In order to reason about programs, we'll need some formal definitions of the different parts of a language and how different kinds of statements can affect assertions.
• For example, if we know that a has the value 2 before we execute the statement `b = a`, what do we know afterwards?
• Similarly, if we want that b has the value 5 after the statement `b = a`, what must we ensure beforehand.
• Weeks seven through eleven will emphasize the semantics of a small language that is close enough to most imperative languages to be useful.
• Finally, we'll see how to apply reasoning and the semantics of a language to program development, which will take most of week twelve.

## Boolean Basics

• Boolean logic was developed by George Boole (although he did not name it as such) as a formal system for studying truth.
• There are only two values in Boolean logic: True and False.
• As in most algebraic systems, there are operations on Boolean values.
• The key unary operation is negation (not).
• The key binary operations are conjunction (and), disjunction (non-exclusive or), implication, and equality.
• Boolean logic is abstract: In addition to referring to the basic values, you can also use variables to represent values.
• What kinds of things can you do in Boolean logic?
• Build propositions, compound Boolean expressions. (Our book gives two different grammars for doing so.)
• Given a state (a mapping of variables to values), evaluate a compound expression, determining whether it is true of false.
• Determine the set of states in which a proposition holds.
• Prove that a proposition always holds. We say that a proposition that always holds is a tautology.
• Disprove that a proposition is a tautology.
• Prove equivalent two different propositions.
• ...
• Can we define the set of all Boolean propositions? Certainly. We normally do so recursively, with a context-free grammer.

### A Simple Boolean Grammar

• True and False are propositions.
• Any variable is a proposition.
• If p is a proposition, (not p) is a proposition.
• If p1> and p2 are propositions, so are
• (p1 and p2)
• (p1 or p2)
• (p1 implies p2)
• (p1 equals p2)
• Nothing else is a proposition.

• As you may have noted, there are many too many parentheses in the language described above.
• As in normal arithmetic, we can use precedence and associativity to eliminate parentheses.
• What precedence would you choose?
• Does associativity matter? If so, which would you choose for each operation?

## Proof and Reasoning

• As you may have noted from our initial consideration of what we might do in Boolean logic, proof is a key activity in working with Boolean values.
• How do you prove that a proposition is a tautology?
• Build a truth table. Building a truth table is time consuming (how much so?) but is guaranteed to give us a correct answer and can be automated.
• Prove that the proposition is equivalent to a simpler proposition, and prove that the simpler proposition is a tautology.
• How do we prove that two propositions are equivalent?

## History

Tuesday, 7 January 2003 [Samuel A. Rebelsky]

• Created generic version to set up course.

Back to Binary Search. On to The Structure of a Computer.

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Fri May 2 14:20:09 2003.
The source to the document was last modified on Mon Jan 20 12:41:00 2003.
This document may be found at `http://www.cs.grinnell.edu/~rebelsky/Courses/CS195/2003S/Outlines/outline.03.html`.

You may wish to validate this document's HTML ; ; Check with Bobby

Samuel A. Rebelsky, rebelsky@grinnell.edu