| Predicate Logic for Specifying Programs and Proving their Correctness |
| Program Specification |
| Pre- and Post- Conditions |
| Uses of Specification |
| Specification Example |
| The Need for ÒAnchorsÓ |
| Specification Examples |
| Specification Examples |
| Examples |
| Example with more-formal Logic |
| Forms of Correctness |
| Forms of Correctness |
| Example |
| Slide 14 |
| Squaring Program Idea |
| Synthesis of Squaring Program |
| Synthesis of Squaring Program |
| Prove the Squaring Program |
| Using Primed Variables |
| Using Primed Variables |
| Transition Induction |
| Loop Invariant Positioning |
| Energy Function Principle
for Proving Termination |
| Exercise: Prove this ÒcubingÓ program |
| Example |
| Search Program Specification |
| Note |
| A Search Program |
| Adding Input and Output Assertions (shown in red) |
| Globalizing an Assertion |
| Adding Intermediate Assertions (1) |
| Adding Intermediate Assertions (2) |
| Adding Intermediate Assertions (3) |
| Adding Intermediate Assertions (4) |
| Proving the Assertions (1) |
| Proving the Assertions (2) |
| Proving the Assertions (3) |
| Proving the Assertions (4) |
| Proving the Assertions (5) |
| In more detail (pay careful attention to < vs. <) |
| Proving the Assertions (6) |
| Proving the Assertions (8) |
| Thought Exercise |
| Structural Induction |
| Structural Induction for Lists |
| Structural Induction Example |
| Structural Induction Proof: Basis |
| Structural Induction Proof: Induction Step |
| Fine Points |
| Undecidability |