Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

La sémantique du langage Python
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 11 Sep 2014 13:51
Message La sémantique du langage Python
Petit à propos informel et personnel, en guise de présentation du sujet.

Quand j’ai ouvert les sections sur trois langages informatiques en particulier me semblant parmi les plus importants et pertinants (hors langages de présentation et de données), Ada, Prolog et SML, j’ai fait une sélection serrée en excluant volontairement les langages dont je juge qu’ils ont causé du tord à la considération due à la conception des logiciels (ce domaine est également malmené par la « culture » et la politique, en plus), et Python fait ou faisait (je ne sais pas encore si je dois le dire au passé) parti de ces langages auquel j’ai des reproches sérieux à faire (en soulignant encore que c’est une introduction informelle et sur un ton personnelle).

Depuis sa révision qui date tout de même de 2008 mais qui tarde à s’imposer, des aspects pratiques (ex. les textes sont Unicode par défaut et partout ou cela est raisonnable) et sémantique (ex. la hiérarchie des classes devenue aussi nette et propre que dans le vieux et vénérable Smalltalk) ont cependant été dans le bon sens, ce qui m’a amené à réviser ces mauvaises appréciations (je note quand‑même que l’efficacité n’est toujours pas au rendez‑vous).

Restait le problème qu’est l’absence de définition(s) claire(s) et formelle(s) de sa sémantique, dont l’absence peut faire se ressentir et quand n’y répondent que les imprécisions et les omissions de la documentation officielle.

Je découvre à l’instant qu’une thèse à été écrite sur ce sujet (voir le lien plus bas), ce qui me rassure et m’a décidé à ouvrir ce sujet, qui présentera des expérimentations (qui viendront dans les jours prochains) mettant en évidence quelques points de sa sémantique. Sans au moins l’existence d’une volonté d’une définition formelle, ces expérimentations n’aurait put inviter qu’au bricolage, et cette barrière est levée.

Thèses et documents sur une sémantique opérationnelle de Python


An executable operational semantics for Python (gideon.smdng.nl) [PDF], Gideon Joachim Smeding, Universiteit Utrecht, 2009.

Gideon Joachim Smeding a écrit : 
Programming languages are often specified only in an informal manner; in the available documentation, the language behavior is described by examples and text. Only the implementation, a compiler or interpreter, describes the exact semantics of constructs. Python is no dierent. It is described by an informal manual and a number of implementations. No systematic, formal descriptions of its semantics are available. We developed a formal semantics for a comprehensive subset of Python called minpy. The semantics are described in literate Haskell.

Traduction a écrit : 
Les langages de programmation sont souvent spécifiés d’une manière informelle; dans la documentation disponible, le comportement du langage est décrit par des textes d’exemples. Seul l’implémentation, un compilateur ou interpréteur, décrit la sémantique exacte des constructions. Python n’est pas différent en cela. Il est décrit par un manuel informel et un certain nombre d’implémentations. Aucune description formelle, systématique, de sa sémantique, n’existe. Nous avons réalisé une sémantique formelle pour un sous ensemble de Python, nommé minpy. Les aspects sémantiques sont décrits en Haskell.


Ce n’est encore pas totalement formel (sémantique exprimée en Haskell), mais c’est déjà une approche.


Autre document, pas une thèse, mais un chantier collectif digne d’autant d’intérêt, toujours sur une sémantique opérationnelle de Python.

Python: The Full Monty — A Tested Semantics for the Python Programming Language (cs.brown.edu) [PDF], auteurs multiples, date non‑précisée.

Auteurs a écrit : 
We present a small-step operational semantics for the Python programming language. We present both a core language for Python, suitable for tools and proofs, and a translation process for converting Python source to this core. We have tested the composition of translation and evaluation of the core for conformance with the primary Python implementation, thereby giving confidence in the fidelity of the semantics. We briefly report on the engineering of these components. Finally, we examine subtle aspects of the language, identifying scope as a pervasive concern that even impacts features that might be considered orthogonal.

Traduction a écrit : 
Nous présentons une sémantique opérationnelle discrète pour le langage de programmation Python. Nous présentons à la fois un langage noyau pour Python, convenant au outils et preuves, et un processus de traduction pour la conversion de source Python dans ce noyau. Nous avons testé la composition de la traduction et de l’évaluation du noyau, être conforme à la principale implémentation de Python, par là donnant bonne confiance en la fidélité de la sémantique. Nous présentons brièvement le processus de conception des ces éléments. Pour finir, nous examinons des aspects subtiles du langage, identifiant la portée des noms comme un sujet délicat ayant un effet même sur des propriétés qui autrement pourraient être considérées orthogonales.



Une autre thèse, plus récente que celle présentée comme premier document, et s’appliquant à Python 3.

A formal semantics of Python 3.3 (fsl.cs.illinois.edu) [PDF], Dwight Guth, Université de l’Illinois, 2013.

Dwight Guth a écrit : 
This thesis demonstrates the ability to formalize the operational semantics of complex programming languages in the K Semantic Framework, which provides an interpreter as well as analysis tools for exploring the state space of programs and performing static reasoning about programs. This is demonstrated by means of a partial semantics for the latest version of the popular Python programming language. With additional effort, this semantics will allow users to reason about Python programs, including sources of nondeterminism in the Python language specification, and formal reasoning about their behavior. While the semantics is incomplete, it is executable and has been thoroughly tested against a number of unit tests, and will be demonstrated to perform as well as the reference implementation of Python, CPython, on those features which have been completed. On these features, it also performs as well as or better than other comparable operational semantics of Python.

Traduction a écrit : 
Cette thèse démontre la faisabilité de la formalisation de sémantiques opérationnelles de langage de programmations complexes, dan s le K Semantic Framework, qui fournit un interpréteur et des outils d’analyse pour explorer l’espace des états des programmes et réaliser des analyses statiques sur les programmes. La démonstration en est faite avec une sémantique partielle de la dernière version du populaire langage de programmation Python. Avec quelques efforts supplémentaires, cette sémantique permettra de raisonner sur les programmes Python, incluant les sources de non‑déterminisme dans la spécification du langage Python, et des raisonnements formel sur leur comportements. Cependant que la sémantique est incomplète, elle est exécutable, et a été largement testée à travers un certain nombre de tests unitaires, et se montrera autant efficace que l’implémentation de référence de Python, CPython, pour les propriétés ayant été finalisées. Pour ces propriétés, elle est aussi autant, quand ce n’est pas plus, efficace, que les autres sémantiques opérationnelles de Python comparables.



Plus formelle, par nature, car réalisé dans le cadre du système de preuves formelles Isabelle / HOL (dont il a été question, au moins implicitement, dans le sujet sur les logiques appliquées à l’informatique) : A Semantics of Python in Isabelle/HOL (cs.uregina.ca) [PDF], James F. Ranson, Howard J. Hamilton et Philip W. L. Fong, Université de Regina, 2008.

Auteurs a écrit : 
[…] In this report, we develop a formal definition for a programming language called IntegerPython, which is a subset of the Python language that supports integers, booleans, global variables, loops, modules, and nested functions. The definition takes the form of an operational semantics on a CEKS machine, which we embed in the Isabelle/HOL mechanized logic. We then prove an invariant of the CEKS machine in Isabelle/HOL. The report concludes with strategies for the efficient, executable implementation of the IntegerPython semantics and its extension into a semantics of the entire Python language

Traduction a écrit : 
Dans ce document, nous présentons une définition formelle d’un langage nommé IntegerPython, qui est un sous‑ensemble du langage Python, avec support pour les entiers, booléens, variables globales, boucles, modules et fonctions imbriquées. La définition a la forme d’une sémantiques opérationnelles dans une machine de CEKS, que nous incluons dans la logique de Isabelle / HOL. Le document se conclue par des stratégies pour une implémentation exécutable efficace de la sémantique de IntegerPython et ses extensions, dans la sémantique du langage Python tout entier.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]

Dernière édition par Hibou le Ven 12 Sep 2014 20:45, édité 9 fois.

Ajout d’une référence

Profil Site Internet
zen
Modératrice
Avatar de l’utilisateur
  • Genre : Fille
  • Age : 55
  • Localisation : Un pied dans l'eau et un sur le mont.
  • Messages : 11010
Ven 12 Sep 2014 19:45
Message Re: La sémantique du langage Python
Hibou est un Serpentar, il connait le langage des serpents !
Fait l’innocent(e) Hihihi!
Profil
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mer 24 Sep 2014 21:58
Message Re: La sémantique du langage Python
Hibou a écrit : 
Restait le problème qu’est l’absence de définition(s) claire(s) et formelle(s) de sa sémantique, dont l’absence peut faire se ressentir et quand n’y répondent que les imprécisions et les omissions de la documentation officielle.

En même temps, c’est un effet de la culture qui tourne autour de ce langage, comme en témoigne cet extrait d’un échange représentatif, sur une mailing‑list :

Documenting formal operational semantics of Python (mail.python.org). Mars 2008.

Gideon Smeding a écrit : 
In the context of a master's thesis I'm currently looking into Python's operational semantics. Even after extensive searching on the web, I have not found any formal model of Python. Therefore I am considering to write one myself.

Réponse de Paul Rubin a écrit : 
I doubt if anything serious has been done in that area, and I don't think Python culture operates like that very much. Python programming tends to use informal processes with a lot of reliance on test-driven development and unit tests, rather than formal specifications. A lot of the operational behavior that people rely on basically comes from accidents of implementation, e.g. file descriptors being closed automatically when the last reference goes away. But of course that should not be included in a formal semantics, yet that means the semantics wouldn't describe actual production programs out there.


Je ne traduis pas, mais je résume quand‑même. En mars 2008, un universitaire préparant une thèse, se renseigne sur les définitions de Python, trouvant celles existantes trop peu précises pour une analyse rigoureuse. Quelqu’un lui répond qu’il doute que ce qu’il cherche existe ou ait été entrepris, parce que ce n’est pas trop dans l’esprit de la culture du milieux.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet