Topic outline

  • Forums

    Collapse all Expand all

  • Course description

    • Lecturer : Tarek Boutefara (t_boutefara@univ-jijel.dz)
    • Coefficient : 2
    • Credits : 4
    • Weekly class time :
      • One lecture session (1h30)
      • One tutorial session(1h30)
    • Personal work required per week : 1h00
    • Assessment methods :
      • Written exam : 60%
      • Continuous assessment : 40%
        • Homework
        • Attendance
        • In class short time exams

  • Learning outcomes

    The aim of this course is to present some formal approaches to the specification of programming languages. These methods are used to prove programs, i.e. to demonstrate their validity.
    Unlike unit testing methods, formal methods rely on non-classical logic and lambda calculus (formal systems) to specify the semantics of a programming language, which can then be used to write a ‘proof’ for a program written in the language in question.


  • Prerequisites

    Before being able to study program proofs using formal semantics, it is important to remember the following basic notions:

    • The notion of software (and program) as the main object resulting from a Software Engineering process.
    • The notion of programming language. This notion is itself dependent on several other notions such as: programming paradigm, interpretation/compilation and instruction.
    • Van neu Mann's architecture and the Turing Machine. This leads us to the notion of Computability.
    • Classical mathematical logic.

  • Course content

    • Introduction to Lambda-Calculus,
    • Classical and Intuitionist Logic,
    • Notion of Semantics,
    • Formal expression of semantics.

  • Chapter 00: Reminder

  • Chapter 01: Formal Systems and Lambda Calculus

  • Chapter 02: Hoare Logic

  • Chapter 03: Programming Language Fromal Semantics

  • Chapitre 04 : Expression formelle de la sémantique

  • Références

  • Examens et Corrigés