Département Informatique
PRESENTATION       FORMATIONS       DEPLOIEMENTS NATIONAUX       PUBLICATIONS       RECHERCHE       MEMBRES       CONTACTS



Format d'impression Accessibilité malvoyants (Format Texte)  
Accueil > FORMATIONS > Unités d’enseignements (UEs) et supports > Unités d’enseignements (UEs) > AISL > NFP108 : Spécification et Modélisation Informatiques
Supports de cours

 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 (sep 2018) :

 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



Documents joints:
Calcul des propositions
(PDF - 280.9 kio)
Prédicats et ensembles (Chapitre 3 et 4 des notes)
(PDF - 211.2 kio)
examen 2005 2006
(PDF - 27.6 kio)
bibliographie (bibliographie plus complete)
(PDF - 25.5 kio)
presentation_openfst.zip
(ZIP - 86.7 kio)
dates_fst.zip
(ZIP - 1.6 Mio)
Contacts      CEDRIC      CNAM      Réseau CNAM      Bibliotheque      Handi'CNAM      CRAP      ENJMIN      Mentions légales
FORMATIONS

Informations générales
S’inscrire
Financer sa formation
Licences
Masters
Diplômes d’Ingénieur
Formation doctorale
Titres, diplômes et certificats d’établissement
Alternance
Stages entreprises
Auditeurs
Unités d’enseignements (UEs) et supports
VIE PRATIQUE

Actualités
La Minute Informatique
Revue de presse
Espace privé