NFP120 : Spécification logique et validation des programmes séquentiels

Fiche descriptive de l'UE: Cliquez ici
Diplômes:  CYC45 Diplôme d’ingénieur Cnam spé. informatique option architecture et ingénierie des systèmes et des logiciels , CYC47 Diplôme d’ingénieur Cnam spé. informatique option informatique modélisation optimisation , CYC14 Diplôme d’ingénieur Cnam spé. informatique option réseaux, systèmes et multimédia , CYC12 Diplôme d’ingénieur Cnam spé. informatique option systèmes d’information (ISI) , LG004 Licence STIG, mention informatique générale , CPN11 Titre RNCP (niveau II) concepteur en architecture informatique
REMPLISSEZ LE FORMULAIRE D'APPRECIATION DES AUDITEURS SUR L'ENSEIGNEMENT

Responsable national : Pierre Courtieu

Attention : Cette UE est fermée au Centre d’Enseignement de Paris depuis 2016.

Cours 2015 :Olivier Pons et Tristan Crolard

Cette année encore nous allons mutualisé les premières séances de ce cours avec le cours NFP101. Nous ferons donc cours dans la salle prévue au départ pour NFP101 en début de semestre puis nous séparerons les deux groupes dans deux salles différentes.

Cette année, et comme les deux dernières, nous ne pratiquerons pas plus Proolog. Les raisons de ce changement sont expliquées dans le document de cours ci-après.

En revanche un nouvel outil sera utilisé pour présenter les cours : l’outil Coq. CEPENDANT COQ NE SERA JAMAIS UTILISÉ PAR LES ÉTUDIANTS, il ne s’agit que d’un support pour présenter les notions du cours. Les supports de cours sont des fichiers au format PDF extraits des développements coq. Vous n’avez donc pas besoin de Coq pour les lire. En cours ces développements seront parfois présentés de manière plus interactive à l’aide de Coq.

Coq est un assistant de preuve. Autrement dit c’est un logiciel dans lequel l’utilisateur peut écrire des définitions mathématiques formelles, dans un style ressemblant à la programmation, et effectuer des démonstrations sur ces définitions. Le cadre formel est contraignant et la syntaxe rigide mais assurent que les démonstrations sont correctes. Nous utiliserons donc cet outil comme un format uniforme et rigoureux de définition.

- Supports de cours 2014-2015

- Feuilles d’exercices

- Annales

- Feuilles d’exercices

- Annales