Programmé en UV2 MAJ INF, UV2MAJ INFMS
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 2017/2018
Dernière mise à jour le 25-APR-17
Validation par le responsable de programme le
|
