Programmé en UV2MAJ INFMS, UV2 MAJ INF
Présentation :
La logique et la théorie des langages font partie des fondements de l'informatique. Dans ce module nous allons aborder certaines notions de ces théories.
Un langage est un ensemble de «mots» définis sur un «alphabet». Les expressions régulières (que l'on retrouve dans tous les langages de programmation modernes) sont un moyen de définir une classe particulière de langages, appelés langages réguliers. Les automates en donnent une description analytique (un mot appartient à un langage s'il peut être obtenu par une suite de transitions entre états de l'automate) et les grammaires formelles une description générative (un mot appartient à un langage s'il peut être obtenu par une suite de productions à partir d'un axiome de départ).
La logique étudie les principes du raisonnement. Dans ce cours, nous allons nous restreindre à deux types de logique : la logique propositionnelle et la logique des prédicats.
Une proposition est une phrase qui peut être vraie ou fausse. En logique propositionnelle on étudie les règles qui permettent de prouver la vérité d'une proposition à partir de celles d'autres propositions.
La logique des prédicats ou logique de premier ordre est une formalisation du langage des mathématiques. Elle utilise des fonctions, des variables, des prédicats, des connecteurs et des quantificateurs, groupés en formules. Il s'agit de prouver des formules mais aussi d'étudier les liens entre des structures mathématiques et informatiques (appelées des modèles) et des ensembles de formules logiques (appelés des théories).
Enfin, la logique du premier ordre permet de définir la sémantique des langages de programmation et de vérifier leur correction.
Objectifs pédagogiques :
- Comprendre les notions d'automate, de langage formel, d'expression régulière, de grammaire formelle
- Utiliser les expressions régulières dans plusieurs contextes
- Démontrer des propositions logiques
- Démontrer des formules de logique de premier ordre
- Insérer des assertions dans un programme et les vérifier
Volume horaire :
18h
Contenu détaillé :
C/TP-LF1 (3 h) : Langages formels, langages réguliers, expressions régulières
C/TP-LF2 (3 h) : Automates d'états finis
C/PC-LF3 (3h) : Grammaires formelles
C/PC-LOG1 (3h) : Logique propositionnelle
C/PC-LOG2 (3h) : Logique de premier ordre
C/PC-LOG3 (3h) : Sémantique et vérification des langages de programmation
Travaux personnels encadrés :
TP-LF1 (1h30) : Expressions régulières sous Python
TP-LF2 (1h30) : Automates d'états finis (travail à rendre)
PC-LF3 (1h30) : Expressions régulières, automates, grammaires
PC-LOG1 (1h30) : Exercices en logique propositionnelle
PC-LOG2 (1h30) : Exercices en logique du premier ordre
PC-LOG3 (1h30) : Exercices de vérification de petits programmes
Année 2018/2019
Dernière mise à jour le 10-JAN-18
Validation par le responsable de programme le
|