Študijné materiály pre kurz 1-AIN-470 Špecifikácia a verifikácia programov LS 2013/14

Specification and Verification of Programs

• Preliminaries

• Formal System

• Propositional Logic

• The Method of Propositional Tableaux
• Quantification Logic
• Peano Arithmetic

• Program Correctness

• Numeric Programs

• Explicit Definitions
• Primitive Recursion
• Course of Values Recursion
• Recursion with Measure
• Tail Recursion and Iteration
• Recursion on Notation
• Case Study: Integer Square Root
• Exercises

• Programs Operating on Word Domains

• Dyadic Words
• Exercises

• Programs Operating on Lists

• Lists
• Basic Operations
• Sorting of Lists
• Exercises

• Programs Operating on Trees

• Binary Trees
• Binary Search Trees
• Exercises

• Programs Operating on Symbolic Expressions

• Numeric Terms
• Exercises