Getting it Right
Writing correct programs involves solving two very difficult problems.
- Saying what you want the program to do.
- Convincing someone (possibly yourself) that your program does what you say it does.
This course explores some of the fundamental tools that computer science gives us to reason about the correctness of programs. This course is based on my experience teaching the introductory data structures course at Carnegie Mellon.
Either the Computation or Change course or some experience writing programs with loops and functions that call each other.
After this course, you'll be able to answer questions like:
- How do I prove a program is correct?
- How do I prove that a program is incorrect?
- What does partial and total correctness mean?
- How do we prove correctness of a function with loops and recursive calls?
- What is a contracts and how do contracts help us prove programs correct?