Sémantique des Languages
مخطط الموضوع
-
-
Posez vos questions ici.
-
الملف
A remettre avant 04/12/2023. Ce devoir est évalué sur 2 points.
-
الملف
A remettre avant 23/12/2023. Ce travail est évalué sur 2 points.
-
- Chargé du cours : Tarek Boutefara (t_boutefara@univ-jijel.dz)
- Coefficient : 2
- Crédits : 4
- Volume horaire présentiel :
- une sénace du cours (1h30)
- une séance TD (1h30)
- une sénace du cours (1h30)
- Volume horaire de travail personnel requis/semaine : 1h00
- Modalité d'évaluation :
- Examen écrit : 60%
- Evaluation continue : 40%
- Devoirs
- Assiduité
- Interrogation
-
L'objectif de ce module est de présenter quelques approches formelles pour la spécification des langages de programmation. Ces méthodes sont utilisées pour prouver des programmes, c'est-à-dire, pour démontrer sa validité.
Contrairement aux méthodes de test unitaire, les méthodes formelles s'appuient sur des logiques non-classiques et sur le lambda-calcul (les systèmes formels) pour spécifier la sémantique d'un langage de programmation ce qui permet, par la suite, d'écrire une "preuve" pour un programme écrit dans le langage en question.
-
الصفحة
-
-
Avant de pouvoir étudier les preuves des programmes en utilisant la sémantique formelle, il est important de se rappeler des notions de base suivantes :
- La notion du logiciel (et de programme) comme étant l'objet principal résultant d'un processus Génie Logiciel.
- La notion du langage de programmation. Cette notion est elle-même dépend de plusieurs autres notions comme : paradigme de programmation, interprétation/compilation et instruction.
- L'architecture de Van neu Mann et la Machine de Turing. Ce qui nous conduit à rappeler la notion de Calculabilité.
- Logique mathématique classique.
-
- Initiation au Lambda-Calcul,
- Logique classique et Intuitionniste,
- Notion de Sémantique,
- Expression formelle de sémantiques.
-
الصفحة
-
-
La logique constructive est le sujet du premier devoir.
-
الملف
-
-
-
الملف
-