Département Informatique

Accueil > UES > UEs par domaine > AISL NFP120 : Spécification logique et validation des programmes séquentiels
s'abonner à cette rubrique Envoi vers Viadeo Envoi vers Twitter Envoi vers LinkedIn Envoi vers Facebook Format d'impression Accessibilité malvoyants (Format Texte)  

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

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

  • Exercices sur les tableaux sémantiques
  • Exemples d’examens similaires utilisé en ED (anciens examens de NFP209, donc un peu plus durs que ce qui sera demandé pour NFP120). 2008 2009 2010. Toutes les corrections ne sont pas présentes pour l’instant mais pour la logique de Hoare en particulier elles y sont..
  • TP 1 frama-c/jessie (Exercice : prouver les programmes suivants dans frama-c). Référence rapide sur jessie (en anglais) : ici.

- Annales

- Feuilles d’exercices

- Annales


Contacts | FORUMS | CEDRIC | CNAM | Réseau CNAM | Mentions légales