Séance de cours

Vérification automatique des exercices de programmation

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

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 (16)

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 (10)

Itérations : Concepts et exemples avancés

Couvre les concepts avancés d'itérations en C++, y compris différentes formes de boucles et d'erreurs communes à éviter.

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 de programmation et itérations Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre les concepts fondamentaux des boucles et itérations dans la programmation, y compris les boucles conditionnelles, pour les boucles, tandis que les boucles, cassent et poursuivent les énoncés.

Hoare Logic: Fondements et applications

Couvre Hoare Logic, ses fondements, ses applications et son importance dans la vérification des programmes.

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.

Afficher plus

Concepts associés (16)

Logique de Hoare

Vérification formelle

Correction d'un algorithme

Foreach loop

Boucle while

Afficher plus