IF105 (Springs 2012 & 2013)

Undergraduate Tutorial sesssions, ENSEIRB-MATMECA, Department of Computer Science, 2012

The aim of the course is to acquire theoretical tools in order to build formal reasonings, and to prove the termination and the correction of algorithms.

Syllabus

  1. Logic
    • Formalization in first-order logic
    • Introduction to proof theory
    • Induction, proof by induction
  2. proofs of algorithms
    • Specification through pre and post conditions
    • While-programs, semantics
    • Proof of correctness, Hoareā€™s logic
    • Termination proof: well-founded sets