– INFORMATIONS :

Informations les années à venir

Cette UE n’ouvrira pas cette année, faute d’un nombre suffisant d’inscrits.
Une ouverture est possible si un nombre conséquent d’intentions d’inscription sont envoyées à Pierre.Courtieu(a)lecnam.net.

– INFORMATIONS : 2020-2021

page moodle 2020-2021

EXAMEN : L’examen consistera en un devoir fait à la maison, inspiré des sujets d’examens habituels.

LE SUJET EST SORTI

sujet. À rendre avant le 14 février 2021 minuit (par mail à Pierre.Courtieu@gmail.com).
DATE DE PUBLICATION DU SUJET : 6 février.
DATE LIMITE DE RENDU : 13 février à minuit.

Le Cnam étant fermé en raison de la crise sanitaire,
à partir du Mardi 3 Novembre 2020 les cours auront lieux en visio (synchrone à l’heure du cours) et/ou juste a distance (asynchrone avec des vidéos enregistrée).

Vous avez dû recevoir un lien Teams via moodle pour le cours de ce mardi 18h15.

Notes de Cours
– logique
– Automates
– Annotation de programme, Logique de Hoare
– Annales
– Archives

Partie Logique (O. Pons)

Ebauches de notes de cours de logique en cours de mise à jours (perpétuellement ;-)) :

– partie1 : Poly Intros, langages, propositions,
slide intro
slide propositions

– partie 2 :Prédicats et Théorie des ensembles
– regles de deduction naturelles

Premières feuilles d’exercices de logique :
– feuille 1
, corrigé

– feuille 1 bis
, corrigé

– feuille 2
, corrigé

– feuille 3
, corrigé

– feuille 4
, corrigé

– feuille de revision
, corrigé

– revision et predicat en DN (avec corrigé)

Ancienne feuilles
– WP
, corrigé

Le sujet du TP sur la déduction naturelle et son corrige

Le démonstrateur utilisé est disponible

Partie Automates

ATTENTION CHANGEMENT 2018 : Pierre Courtieu reprend cette partie du cours et le contenu a changé

– Notes de cours sur les automates (F. Barthélémy)
– Slides sur les automates (P. Courtieu) <== Mis en ligne le 1er déc 2020. Ces slides sont en accord avec les notes de cours ci-dessus. Elles couvrent en partie les chapitres 1 à 7. Les transducteurs sont hors-programme.

Les premières feuilles d’exercices :
– feuille 1notes prises pendant le cTD : Ex. 1 et 2, Ex. 3 Ex. 4-5
– feuille 2 Notes prises : Ex. 1
– feuille 3Notes prises : Ex
– feuille 4
– feuille 5

Pour la culture générale sur les automates :
– Vidéo de cours sur un automate de la norme TCP (excusez la qualité sonore)
– Document complémentaire : la norme RFC793

Des exercices supplémentaires usr les automates :
– Énoncé de l’exercice sur HTTP
– Commentaire sur l’énoncé de l’exercice (vidéo)
– Faites l’exercice avant de consulter le corrigé. corrigé de la question 1
corrigé de la question 2
– Il y a un exercice sur les regexp dans l’espace NFP108 de pleiad avec correction automatique. Connectez-vous via https://lecnam.net

– Lien vers le cours UML de Laurent Audibert (sur developpez.com).
C’est surtout le chapitre 5 sur les diagrammes d’états-transitions qui nous intéresse.

Nouvelle série :
– exercices sur les automates
– exercices sur la modélisation par automates
– exercices sur les expressions régulières
– exercices sur la modélisation par expressions régulières

Pour approfondire (les tranducteurs ne sont pas au programme mais il y a aussi des exercices sans transducteur) :
– feuille 6
– feuille 7
– feuille 8
– feuille 9
– feuille 10
– exercices sur les transducteurs

Partie annotation logique de programme — Logique de hoare

Cette (nouvelle) partie est une introduction à une approche logique de la
programmation. Le *cours* montre comment on peut démontrer logiquement
qu’un programme vérifie sa spécification, à l’aide de formules logiques et
d’un système de déduction (comparable à celui de la déduction naturelle
par exemple) : la logique de Hoare.

*Cependant* vous ne serez pas interrogés sur la partie "preuve de programme", en
revanche il vous sera demandé d’écrire des formules logiques de spécification
et des variants et invariants de boucles.

Support de cours sur la logique de Hoare :
slides
slides annotés

Une feuille d’exercice d’annotations :
feuille 1
sujet annoté
sujet annoté (2)
annotation (3) (notamment algo de Dijsktra sur les graphes)
solution recherche dans un tableau (feuille 1)

Annales

– première session 2018/2019. corrigé Zeus et automate corrigé formule
annale annotée jan 2021
– seconde session 2016/2017
– première session 2016/2017
– seconde session 2015/2016
– première session 2015/2016
– seconde session 2014/2015
– seconde session 2013/2014
– première session 2013/2014
– seconde session 2010/2011
– seconde session 2009/2010
– première session 2009/2010

Archives

Quelques ressources sur les automates :
– support de cours sur TCP
– norme TCP (RFC793)
– document sur l’implémentation des automates
– document complémentaire sur les transducteurs

TP sur les automates
– Le sujet du TP sur les automates finis.
– Le sujet du TP python.
– Le sujet du TP sur l’extraction d’information (nouvelle version).
– Le sujet du TP sur l’extraction d’information (ancienne version).
– Le sujet du TP sur les expressions régulières en Java.

Projet sur les transducteurs
Vous trouverez ci-dessous des documents des années précédentes.
– Le sujet du projet.
– Le fichier de symboles ISO-8859-1
– L’automate représentant l’union de tous les caractères de l’alphabet (format texte)
– Une page d’accueil du monde compilée en automate (forme texte)
– Un script python pour compiler une page du monde
– Pour rendre le projet, il y a un formulaire sous une plateforme de télé-enseignement appelée Moodle. Pour accéder à ce formulaire, il faut utiliser vos identifiants et mots de passe du CNAM (les mêmes que pour le TP, pas ceux de pleiad). Lorsque vous arrivez sur la plateforme, vous devez faire une opération appelée "inscription" au cours. Il ne s’agit pas de votre inscription administrative, mais juste de vous enregistrer sous Moodle comme suivant le cours NFP108. Ensuite vous avez accès au formulaire de remise du devoir.
Accès au formulaire ici.
Si vous n’avez pas vos identifiants ou mots de passe, consultez 
le site http://ressources-informatiques.cnam.fr

TP sur les automates

– Le sujet du TP sur les automates finis.
– Télécharger FSM
– Télécharger Lextools (pour linux)
– Télécharger graphviz

Devoir sur les automates

Un délai est accordé : vous pouvez remettre votre devoir jusqu’u dimanche 29 janvier 2012.
– Enoncé du devoir
– Pour remettre votre devoir et pour utiliser le webservice lextools et fsm, il faut vous identifier avec votre login et votre mot de passe du cnam. Si vous ne les connaissez pas, consultez :
ressources-informatiques.cnam.fr
– webservice lextools et fsm
– démo du webservice
– page d’annonces (exemple pour le devoir, convertie en ISO-8859-9)
– lien sur une page réelle du même genre
– complément sur les transducteurs en lextools et fsm
– formulaire de remise du devoir
– explications à propos de votre identifiant et de votre mot de passe
– formulaire pour obtenir votre mot de passe

Devoir sur les automates

– Enoncé du devoir
– formulaire de remise du devoir
– explications à propos de votre identifiant et de votre mot de passe
– formulaire pour obtenir votre mot de passe

Devoir sur les automates

– Enoncé du devoir

Devoir logique

– Enoncé du devoir 2
– formulaire de remise du devoir

Devoirs 2007/2008

A titre indicatif, voici les énoncés des devoirs de l’an dernier.

– énoncé du premier devoir de l’an dernier

– énoncé du second devoir de l’an dernier

TP 2007/2008

Le sujet du TP sur la déduction naturelle

Le démonstrateur utilisé est disponible

corrige du TP

Notes de cours des années antérieures

Vous trouverez ici les notes de cours de l’année passée, données à titre
indicatif. Le cours est susceptible d’évoluer et les notes de cours seront mises à jour.

Notes sur le calcul des propositions
ici

Notes sur le calcul des prédicats et
la théorie des ensembles ici

Vous pouvez trouver le devoir de l’année 2005/2006
ici

Bibliographie

Un livre assez proche de l’approche faite en cours :
Mathématiques discètes appliquées à l’informatique. Rod Haggarty, Coll Synthex , Pearson Education.

Pour les premiers chapitres sur la Theorie des Ensembles :
Program Derivation : The Development of Programs from Specifications
de Geoff Dromey, Addison-Wesley (mars 1989) ISBN : 0201416247

une bibliographie plus complète
ici
test