Rechercher une ressource pédagogique : preuve de programme

Le moteur de recherche des ressources pédagogiques donne accès à un ensemble de documents mis à disposition par l'Université Numérique, les établissements d'enseignement supérieur et Canal U. Vous y trouverez des productions universitaires dans l'ensemble des domaines de formation.

FILTRES

9 résultats
section 1 sur 1
résultats 1 à 9
UNIT
UNIT
07.01.2009
Approches fonctionnelles de la programmation
Description : Fournir un panorama complet du paradigme de programmation fonctionnelle et de son positionnement par rapport aux autres paradigmes de programmation (en particulier de la programmation impérative). Illustrer l'ensemble des concepts abordés au moyen de deux langages fonctionnels: Lisp et Haskell.
  • fuscia
  • Lisp
  • Haskell
  • preuve de programme
UNIT
UNIT
28.11.2008
Demandez le programme
Description : La programmation consiste à décomposer un algorithme en ordres simples et à les écrire en un langage compréhensible par l’ordinateur.
  • bug
  • paradigme de programmation
  • niveau d'abstraction
  • erreur
  • preuve de programme
  • fuscia
UNIT
UNIT
01.08.2011
Du rêve à la réalité des preuves
Description : Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens.
  • assistant de preuve
  • preuve formelle
  • preuve de programme
  • logique mathématique
  • démonstration
  • complexité
  • fuscia
UNIT
UNIT
11.12.2008
La vérité et la machine
Description : Peut-on être sûr de la vérité d’une preuve ? Cette preuve de la preuve, comment l’obtenir en pratique ? La vérification formelle de démonstration est de plus en plus utilisée par les mathématiciens.
  • preuve de programme
  • preuve formelle
  • logique mathématique
  • démonstration
  • Coq
  • théorème des quatre couleurs
  • fuscia
UNIT
UNIT
05.02.2009
Les ingrédients des algorithmes
Description : Pour programmer un ordinateur, le plus important ce sont les méthodes mises en œuvre. Découvrez les ingrédients à combiner pour créer ces algorithmes !
  • algorithme
  • programme
  • séquence d'instructions
  • boucle
  • condition
  • variable
  • fonction
  • langage de programmation
  • erreur
  • preuve de programme
  • indécidabilité algorithmique
  • syntaxe d'un programme
  • sémantique d'un programme
  • fuscia
UNIT
UNIT
21.09.2012
Preuves de programmes en coq
Description : Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique ...
  • Coq
  • assistant de preuve
  • programmation fonctionnelle sûre
  • preuve de programme
  • logique mathématique
  • méthode formelle
  • calcul des constructions
  • correction de logiciel
  • algorithmique certifiée
  • théorie des types
  • logiciel libre
  • récursion
  • fuscia
Canal-U
Canal-U
18.01.2012
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie
Description : Nous présentons les systèmes embarqués critiques et les exigences qui leur sont liées : dans certains cas (nucléaire, avionique, santé) aucun bug n'est accepté. Puis nous présentons l'analyse statique, que nous illustrons sur un exemple de programme. Nous montrons que pour analyser des variables ...
  • algorithmique
  • treillis de Galois
  • preuve de programme
  • analyse de programme
  • sémantique programmation
  • génie logiciel
Canal-U
Canal-U
18.01.2012
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 1ère partie
Description : Nous présentons les systèmes embarqués critiques et les exigences qui leur sont liées : dans certains cas (nucléaire, avionique, santé) aucun bug n'est accepté. Puis nous présentons l'analyse statique, que nous illustrons sur un exemple de programme. Nous montrons que pour analyser des variables ...
  • algorithmique
  • treillis de Galois
  • preuve de programme
  • analyse de programme
  • sémantique programmation
  • génie logiciel
Canal-U
Canal-U
16.06.2009
Pourquoi mon ordinateur calcule faux?
Description : Dans cet exposé Sylvie Boldo nous fait prendre conscience de l'importance des bugs en informatique et des conséquences historiques qu'ils ont pu engendrer. Elle se concentre ensuite sur les problèmes liés aux calculs numériques et montre de manière détaillée et constructive comment prendre la mesure ...
  • bug
  • algorithmique
  • arithmétique flottante
  • calcul informatique
  • méthode formelle
  • nombre à virgule flottante
  • preuve de programme
  • vérification de logiciel