SUNY Geneseo Department of Computer Science

Proofs and Algorithms

Previous Lecture

Misc

ACM meeting Wednesday, 2:30, South 309

Hand in lab 1 today

Questions?

Reading Summary

Sections 3.1 - 3.3, 3.5, 3.6

Theory behind programming

• = mathematical reasoning that leads to and/or verifies correctness of programs

Sequence of thoughts

• Start with preconditions, postconditions
• General idea of what needs to be done
• Then go into theorem
• Then apply

Above is also an outline of how to prove something

Make program correct and efficient, program needs to do what it's supposed to every time in fewest steps

Proving theorem or program correct

Correct means postconditions all met after running program, this must happen every time program runs with preconditions holding

Testing (empirical) vs proving (theoretical) correctness

Logic part, not really related to programming

• (Well, yes it is closely related to understanding programs)
• Can fail if not looked at right, e.g., "some" vs "all"

Modus ponens,"if p then q" allows you to conclude q when you know p is true

Examples

"makeChange" -- demonstrate correctness

Efficiency in terms of robot, e.g., move twice rather than move with some turns in between

Examples, explanation of terms

Find the Northwest Corner

Robot needs to move from arbitrary starting position and orientation to the western-most free tile of the north row, given that another robot is somewhere in the room

Preconditions

• The room contains 2 robots, "hunter" and "obstacle"
• The room has no interior walls
• The room is at least 2 tiles high and wide

Postcondition

• "Hunter" is standing on the western-most free tile of the north row

Design an algorithm...

Prove that it is correct...

See the Java Code we wrote for both the algorithm and its proof. Key things in the process were that we really designed the algorithm and did the proof simultaneously, proof helped keep track of where we were and what issues had to be considered, whether algorithm was doing what we wanted. Proof really just consists of a series of statements about the state of the problem (where the hunter robot is, how it is facing) at various points in the code, with each statement following from previous ones and the results of the intervening statements.

This exercise also demonstrated some other things about design, e.g., importance of identifying an overall strategy before trying to do detailed design, importance of breaking a big problem into sub-problems, each with their own postconditions, etc.

Next

Experimentation in computer science

Read Sections 4.1 - 4.6

Next Lecture