Held: Friday, January 28, 2005
Summary:
Today we begin our consideration of why one might want to formally
define programming languages and verify programs in those languages. We also
begin to consider Boolean logic, the language we will use for defining
and reasoning within programming languages.
Related Pages:
Assignments
- Read C. A. R. Hoare's "Hints on Programming Language Design" (due Wednesday).
- Read chapter 2 of Gries (due Friday).
Notes:
- I was disappointed that not everyone submitted questions.
- I was disappointed that many of you did not take time to spell your questions correctly.
- I do appreciate you trying, though.
- No homework for Monday! I will be absent. You'll watch
Growing a Language
by Guy Steele.
- I've added a Class FAQ. Keep those questions coming.
Overview:
- Background: Why study Gries and The Science of Programming?
- Boolean basics
- A grammar for Boolean propositions
- Boolean proof and reasoning
- As you may have noted in the first reading, one of the key steps in the development of programming languages was the development of precise ways to specify the meaning (semantics) of programs.
- Why do we want to precisely specify the meaning of programs?
- To guide implementers
- To ensure that programs do what programmers expect them to do
- To allow programmers to formally prove the correctness of their programs
- Traditionally, we use Gries's The Science of Programming as an introduction to program verification
- In this class we will also use it to look at how one formally specifies semantics.
- How will we approach Gries?
- 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 four: Assertions about arrays.
- Week six: Using assertions in documentation.
- Week seven: Weakest preconditions
- Week eight: Pause for breath: How do we read Gries?
- Week nine (full week): Defining semantics; continued in week ten
- Week twelve (full week): Using Gries for program development
- 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.
- Week nine covers that key issue for a language similar 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 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.
- True and False are propositions.
- Any variable is a proposition.
- If p is a proposition, (not p) is a
proposition. (Yes, those parentheses are officially required, as are those in the following cases.)
- If p_{1}> and p_{2} are propositions, so are
- (p_{1} and p_{2})
- (p_{1} or p_{2})
- (p_{1} implies p_{2})
- (p_{1} equals p_{2})
- 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?
- 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?