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

Programme

Programmation et logique


- sémantique des formules logique
- méthode de déduction logique: tableaux sémantiques
- sémantique des programmes
- méthode de déduction sur les programme: preuves de Hoare, invariants de boucles
- Application aux programmes Java ou C (assertions, outils de validation)

Objectifs : aptitudes et compétences

Objectifs :

Donner les principes fondamentaux d'une programmation et d'une documentation rigoureuse.
Montrer comment la documentation formelle permet la validation des logiciels.
Remarque: Ce cours comportait précédemment une longue introduction à Prolog, cet aspect du cours a été retiré.

Compétences :

Maitrise de techniques formelles de spécification et de validation de programmes.

Prérequis

Le cours présente progressivement toutes les connaissances requises, néanmoins il est souhaitable d'avoir des notions de logique (propositionnelle, des prédicats). L'UE NFP108 est par exemple une très bonne introduction.

Délais d'accès

Le délai d'accès à la formation correspond à la durée entre votre inscription et la date du premier cours de votre formation.

• UE du 1er semestre et UE annuelle : inscription entre mai et octobre
• UE du 2e semestre : inscription de mai jusqu'à mi-mars

Exemple : Je m'inscris le 21 juin à FPG003 (Projet personnel et professionnel : auto-orientation pédagogique). Le premier cours a lieu le 21 octobre. Le délai d'accès est donc de 4 mois.

Planning

Modalités

Modalités pédagogiques :

Pédagogie qui combine apports académiques, études de cas basées sur des pratiques professionnelles et expérience des élèves. Équipe pédagogique constituée pour partie de professionnels. Un espace numérique de formation (ENF) est utilisé tout au long du cursus.

Modalités de validation :

Examen final

Tarif

Plusieurs dispositifs de financement sont possibles en fonction de votre statut et peuvent financer jusqu'à 100% de votre formation.

Salarié : Faites financer votre formation par votre employeur

Demandeur d'emploi : Faites financer votre formation par Pôle emploi

Votre formation est éligible au CPF ? Financez-la avec votre CPF

Si aucun dispositif de financement ne peut être mobilisé, nous proposons à l'élève une prise en charge partielle de la Région Nouvelle-Aquitaine avec un reste à charge. Ce reste à charge correspond au tarif réduit et est à destination des salariés ou demandeurs d'emploi.

Pour plus de renseignements, consultez la page Financer mon projet formationopen_in_new ou contactez nos conseillers pour vous accompagner pas à pas dans vos démarches.

Passerelles : lien entre certifications

• LG025B31 - Bloc Informatique : Méthodes et outils du génie logiciel
• CRN0802A - Titre RNCP Niveau 6 Concepteur intégrateur d'infrastructures informatiques : Systèmes d'information (SI)
• CRN0801A - Titre RNCP Niveau 6 Concepteur intégrateur d'infrastructures informatiques : Systèmes et réseaux
• CRN0803A - Titre RNCP Niveau 6 Concepteur intégrateur d'infrastructures informatiques : Cybersécurité

Taux de réussite

Les dernières informations concernant le taux de réussite des unités d'enseignement composant les diplômes

Taux de réussite