Séance de cours

Convertir les programmes impératifs en formules

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.

Dans cours

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

Description

Cette séance de cours de l'instructeur couvre le processus de conversion des programmes impératifs en formules, en se concentrant sur la génération de conditions de vérification. Il explique comment exprimer l'exactitude du programme en tant que condition de vérification et l'implémenter en tant qu'algorithme. La séance de cours se penche également sur la représentation des fragments de programme et des spécifications sous forme de formules, introduisant des énoncés impératifs, du non-déterminisme et des programmes sans boucle. Il détaille la construction de formules décrivant les relations entre les états initial et final de l'exécution du programme, y compris les affectations, les instructions if-else et les points-virgules de commande. Des exemples et des formules de calcul sont fournis pour illustrer les concepts.

Enseignant·e

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Source officielle

Proximité ontologique

Informatique théorique

Théorie des langages de programmation: Langage de programmation de haut niveau

Concepts associés (27)

Programmation impérative

En informatique, la programmation impérative est un paradigme de programmation qui décrit les opérations en séquences d'instructions exécutées par l'ordinateur pour modifier l'état du programme. Ce type de programmation est le plus répandu parmi l'ensemble des langages de programmation existants, et se différencie de la programmation déclarative (dont la programmation logique ou encore la programmation fonctionnelle sont des sous-ensembles).

Structure de contrôle

En programmation informatique, une structure de contrôle est une instruction particulière d'un langage de programmation impératif pouvant dévier le flot de contrôle du programme la contenant lorsqu'elle est exécutée. Si, au plus bas niveau, l'éventail se limite généralement aux branchements et aux appels de sous-programme, les langages structurés offrent des constructions plus élaborées comme les alternatives (if, if–else, switch...), les boucles (while, do–while, for...) ou encore les appels de fonction.

Programmation procédurale

En informatique, la programmation procédurale est un paradigme qui se fonde sur le concept d'appel procédural. Une procédure, aussi appelée routine, sous-routine ou fonction (à ne pas confondre avec les fonctions de la programmation fonctionnelle reposant sur des fonctions mathématiques), contient simplement une série d'étapes à réaliser. N'importe quelle procédure peut être appelée à n'importe quelle étape de l'exécution du programme, y compris à l'intérieur d'autres procédures, voire dans la procédure elle-même (récursivité).

Programmation fonctionnelle

La programmation fonctionnelle est un paradigme de programmation de type déclaratif qui considère le calcul en tant qu'évaluation de fonctions mathématiques. Comme le changement d'état et la mutation des données ne peuvent pas être représentés par des évaluations de fonctions la programmation fonctionnelle ne les admet pas, au contraire elle met en avant l'application des fonctions, contrairement au modèle de programmation impérative qui met en avant les changements d'état.

Programmation déclarative

vignette|Binario cropped. La programmation déclarative est un paradigme de programmation qui consiste à créer des applications sur la base de composants logiciels indépendants du contexte et ne comportant aucun état interne. Autrement dit, l'appel d'un de ces composants avec les mêmes arguments produit exactement le même résultat, quel que soit le moment et le contexte de l'appel. En programmation déclarative, on décrit le quoi, c'est-à-dire le problème.

Afficher plus

Séances de cours associées (64)

Convertir les programmes impératifs en formules

Explore la conversion de programmes impératifs en formules, y compris les conditions de vérification, la construction de formules et les structures de flux de contrôle.

Loops : instructions et fonctions de contrôle

Couvre la modélisation des instructions de contrôle avec des fonctions dans Scala, y compris les boucles while, les boucles de répétition et la traduction for-loops.

Fonctions et structures de contrôle en Python

Introduit des fonctions et des structures de contrôle en Python, en soulignant leur importance pour l'organisation et la réutilisation du code.

Programmation Python: Structures et fonctions de contrôle

Couvre des sujets avancés dans la programmation Python, en se concentrant sur les structures et les fonctions de contrôle.

Flux de contrôle en Python : déclarations conditionnelles et boucles

Couvre le flux de contrôle en Python, en se concentrant sur les instructions conditionnelles et les boucles.

Afficher plus

Concepts associés (27)

Programmation impérative

Structure de contrôle

Programmation procédurale

Programmation fonctionnelle

Programmation déclarative

Afficher plus