Sémantique opérationnelle | EPFL Graph Search

Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

En informatique, la sémantique opérationnelle est l'une des approches qui servent à donner une signification aux programmes informatiques d'une manière rigoureuse, mathématiquement parlant (voir Sémantique des langages de programmation). Une sémantique opérationnelle d'un langage de programmation particulier décrit comment chaque programme valide du langage doit être interprété en termes de suite d'états successifs dans la machine. Cette suite d'états est la signification du programme. Dans le cas d'un programme fonctionnel, l'état final d'une suite qui termine donne la valeur de retour du programme. Dans le cas général, il peut y avoir plusieurs suites de calculs et plusieurs valeurs de retour pour un seul programme, parce que celui-ci pourrait être non déterministe. Un des moyens les plus courants pour définir rigoureusement une sémantique opérationnelle est de fournir un système de transition d'états rendant compte du comportement attendu du programme considéré. Une telle définition autorise une analyse formelle du langage, permettant l'étude de relations entre les programmes. Parmi les relations importantes, les pré-ordres de simulation et les bisimulations sont très utiles dans le cadre du parallélisme. Définir une sémantique opérationnelle au travers d'un système de transition se fait habituellement en donnant une définition inductive de l'ensemble des transitions possibles. Habituellement, cela prend la forme d'un ensemble de règles d'inférence définissant les transitions valides du système. Le système devient ainsi représentable sous la forme d'un arbre de dérivation des états du programme lors de l’exécution. La sémantique opérationnelle est reliée à la sémantique dénotationnelle au travers du concept d'abstraction. La syntaxe d'un langage de programmation définit l'ensemble des programmes acceptés par le compilateur lors de la première phase. La sémantique quant à elle vise à donner une interprétation aux programmes construit par cette grammaire.

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

Publications associées (5)

Personnes associées (1)

Concepts associés (25)

Cours associés (6)

Séances de cours associées (53)

MOOCs associés (12)

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 u

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language in

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

The Operational Semantics and Implementation of a Core Dart language

Zhivka Gucevska

In this report we present the specification of the operational semantics of Dart Kernel and a reference implementation of Dart Kernel in Dart. We design a CESK-like machine to specify the operational

2017

Function Passing: A Model for Typed, Distributed Functional Programming

Philipp Haller, Jocelyn Boullier

The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on w

Assoc Computing Machinery2016

Equivalences and calculi for formal verification of cryptographic protocols

Johannes Borgström

Security protocols are essential to the proper functioning of any distributed system running over an insecure network but often have flaws that can be exploited even without breaking the cryptography.

EPFL2008

Couvre Amyli, un petit langage fonctionnel, tapez des règles et de la solidité.

Explore la sémantique relationnelle des boucles dans les programmes et l'interprétation mathématique des structures de boucles.

Explore la sémantique musicale, discute des inférences déclenchées par différents éléments musicaux et propose un cadre pour comprendre le sens de la musique.

(merge of parprog1, scala-reactive, scala-spark-big-data)

In this course you will discover the elements of the functional programming style and learn how to apply them usefully in your daily programming tasks. You will also develop a solid foundation for rea

This advanced undergraduate programming course covers the principles of functional programming using Scala, including the use of functions as values, recursion, immutability, pattern matching, higher-

En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. Comme en linguistique, la sémantique, appliquée aux langages de programmation, désigne le lien entre un signifiant, le programme, et un signifié, objet mathématique. L'objet mathématique dépend des propriétés à connaître du programme. La sémantique est également le lien entre : le langage signifiant : le langage de programmation le langage signifié : logique de Hoare, automates.

Le prix Turing ou ACM Turing Award, en hommage à Alan Turing (1912-1954), est attribué tous les ans depuis 1966 à une personne sélectionnée pour sa contribution de nature technique faite à la communauté informatique. Les contributions doivent être d’une importance technique majeure et durable dans le domaine informatique. La récompense est décernée par l’Association for Computing Machinery (ACM). Cette récompense a été créée par l’InterTrust Technologies Corporation’s Strategic Technologies and Architectural Research Laboratory (STAR Lab).