Convertir les programmes impératifs en formules

Dans cours

Description

Cette séance de cours couvre le processus de conversion des programmes impératifs en formules, en se concentrant sur la génération de conditions de vérification, la construction de formules et l'expression des affectations et des structures de flux de contrôle en tant que relations. Il explique comment représenter l'exactitude du programme en tant que condition de vérification et comment l'implémenter en tant qu'algorithme, en utilisant des exemples dans Stainless. La séance de cours traite également de la traduction d'énoncés impératifs, de choix non déterministes et d'hypothèses en formules. En outre, il explore les concepts de ravages, de programmes sans boucle et de chemins de programme, fournissant des informations sur la construction de formules de taille polynomiale pour décrire les comportements des programmes.

Connectez-vous pour regarder la vidéo

Enseignant

Source officielle

https://mediaspace.epfl.ch/media/0_a525ptjc

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (55)

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).

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.

Switch (instruction)

En programmation informatique, switch (« aiguillage » en anglais), parfois aussi select (comme en VB) ou inspect ou case of (Pascal, Modula 2) ou Match (Rust et Python) est une instruction qui permet d'effectuer un branchement à partir de la valeur d'une variable. Elle peut dans certains cas remplacer une série (souvent peu élégante) de if... else. On l'utilise lorsque les cas à gérer sont nombreux. Ce mécanisme est préfiguré dans les années 1960 par les branchements calculés.