Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Séance de cours

Vérification automatique des exercices de programmation

Description

Cette séance de cours introduit un cadre pour la vérification automatique des exercices de programmation, couvrant des sujets tels que le traitement axiomatique, la représentation par modèle des programmes, les questions de mise en oeuvre et les travaux futurs. Il traite de l'utilisation des contre-exemples, des triples Hoare et des classes spécifiques de programmes en boucle.

Source officielle

Concepts associés (14)

Logique de Hoare

La logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An Axiomatic Basis for Computer Programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction (récurrence) sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare.

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Correction d'un algorithme

Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme.

Foreach loop

In computer programming, foreach loop (or for-each loop) is a control flow statement for traversing items in a collection. is usually used in place of a standard loop statement. Unlike other loop constructs, however, loops usually maintain no explicit counter: they essentially say "do this to everything in this set", rather than "do this times". This avoids potential off-by-one errors and makes code simpler to read. In object-oriented languages, an iterator, even if implicit, is often used as the means of traversal.

Boucle while

vignette|Boucle while En programmation, la boucle while, francisée en boucle tant que, est une structure de contrôle permettant d'exécuter un ensemble d'instructions de façon répétée sur la base d'une condition booléenne. La boucle while peut être considérée comme une répétition de l'instruction if. Une boucle while est constituée d’un bloc de code source et d’une condition. À l’exécution, la condition est d’abord évaluée, et si elle est vraie, le bloc de code source est évalué.

Afficher plus

Séances de cours associées (9)

Programmes de vérification avec l'inox: Partie 2

Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.

Boucles: pendant et pour

Couvre pendant et pour les boucles, y compris les boucles infinies, continuez, passez, et les déclarations de rupture, avec des exemples et des exercices.

Une introduction à l'iris: logique de séparation simultanée d'ordre supérieur

Introduit Iris, un cadre logique pour raisonner sur la sécurité et l'exactitude des programmes impératifs d'ordre supérieur simultanés, en mettant l'accent sur ses caractéristiques et applications uniques.

Boucles conditionnelles: C++ Basics

Couvre les boucles conditionnelles en C++, y compris les boucles 'for' et 'do... while' avec des exemples et une syntaxe.

Boucles : Structures d'itération et de contrôle

Explore les boucles de programmation en C pour la répétition de code, les sorties précoces et le contrôle d'itération, avec des exemples tels que le summing des nombres et la recherche factorielle.

Afficher plus

Concepts associés (14)

Logique de Hoare

Vérification formelle

Correction d'un algorithme

Foreach loop

Boucle while

Afficher plus