IdentifiantMot de passe
Loading...
Mot de passe oublié ?Je m'inscris ! (gratuit)
Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Langages de programmation Discussion :

Présentation de F* : un langage de programmation polyvalent orienté vers la preuve


Sujet :

Langages de programmation

  1. #1
    Communiqués de presse

    Femme Profil pro
    Traductrice Technique
    Inscrit en
    Juin 2023
    Messages
    1 144
    Détails du profil
    Informations personnelles :
    Sexe : Femme
    Localisation : France

    Informations professionnelles :
    Activité : Traductrice Technique

    Informations forums :
    Inscription : Juin 2023
    Messages : 1 144
    Points : 80 104
    Points
    80 104
    Par défaut Présentation de F* : un langage de programmation polyvalent orienté vers la preuve
    Présentation de F* : un langage de programmation polyvalent orienté vers la preuve, prenant en charge à la fois la programmation purement fonctionnelle et la programmation avec effet.

    Voici la présentation de F*. F* est un langage de programmation polyvalent orienté vers la preuve, qui prend en charge à la fois la programmation purement fonctionnelle et la programmation avec effet, et qui combine la puissance d'expression des types dépendants avec l'automatisation de la preuve.

    F* est un langage de programmation à types dépendants qui vise à jouer plusieurs rôles :

    • Un langage de programmation général, qui encourage la programmation fonctionnelle d'ordre supérieur avec des effets, dans la tradition des langages de la famille ML.
    • Un compilateur, qui traduit les programmes F* en OCaml ou F#, et même en C ou Wasm, pour exécution.
    • Un assistant de preuve, qui permet d'énoncer et de prouver les propriétés des programmes.
    • Un moteur de vérification de programmes, exploitant les solveurs SMT pour automatiser partiellement les preuves de programmes.
    • Un système de métaprogrammation, supportant la construction programmatique de programmes F* et les procédures d'automatisation des preuves.


    Pour atteindre ces objectifs, la conception de F* s'articule autour de quelques éléments clés, décrits ci-dessous. Tout cela n'a peut-être pas de sens pour vous - ce n'est pas grave, vous l'apprendrez au fur et à mesure.

    • Un langage central de fonctions totales avec des types dépendants complets, y compris une forme extensionnelle de conversion de type, des types inductifs indexés et des correspondances de motifs, des fonctions récursives avec une vérification sémantique de la terminaison, des types de raffinement dépendants et un sous-typage, ainsi qu'un polymorphisme sur une hiérarchie prédicative d'univers.
    • Un système d'effets indexés définis par l'utilisateur, pour modéliser, encapsuler et raisonner statiquement sur diverses formes d'effets informatiques, y compris une notion primitive de récursivité et de divergence générales, ainsi qu'un système ouvert d'effets définis par l'utilisateur, avec des exemples comprenant l'état, les exceptions, la concurrence, les effets algébriques, et plusieurs autres.
    • Un encodage intégré d'un fragment classique de la logique de F* dans la logique de premier ordre d'un solveur SMT, permettant à de nombreuses preuves d'être automatiquement déchargées.
    • Une réflexion au sein de F* sur la syntaxe et l'état de la preuve de F*, permettant aux programmes Meta-F* de manipuler la syntaxe et les objectifs de preuve de F* et aux utilisateurs de construire des preuves de manière interactive avec des tactiques.


    Nom : 1.jpg
Affichages : 46785
Taille : 10,1 Ko

    DSLs intégrés dans F*

    En pratique, plutôt qu'un langage unique, l'écosystème F* est aussi une collection de langages spécifiques à un domaine (DSL). Une utilisation courante de F* est d'y intégrer des langages de programmation à différents niveaux d'abstraction ou pour des tâches de programmation spécifiques, et de concevoir le langage intégré avec un raisonnement spécifique au domaine, une automatisation des preuves et des backends de compilation. Voici quelques exemples :

    • Low*, un DSL peu profond pour la programmation séquentielle avec un modèle de mémoire de type C comprenant une gestion explicite de la mémoire sur la pile et le tas ; une logique Hoare pour la correction partielle basée sur des cadres dynamiques implicites ; et un backend personnalisé (Karamel) pour compiler les programmes Low* en C pour une compilation ultérieure par des compilateurs C disponibles dans le commerce.
    • EverParse, une intégration peu profonde d'un DSL (superposé au DSL Low*) de combinateurs d'analyseurs syntaxiques et de sérialiseurs, pour les formats binaires de bas niveau.
    • Vale, un DSL profondément intégré pour la programmation structurée dans un langage d'assemblage défini par l'utilisateur, avec une logique Hoare pour une correction totale, et une imprimante pour émettre des programmes vérifiés dans une syntaxe d'assemblage compatible avec divers assembleurs standard.
    • Steel, une intégration peu profonde de la concurrence en tant qu'effet dans F*, avec une logique de séparation concurrente extensible pour la correction partielle en tant que logique de programme de base, et l'automatisation de la preuve construite en utilisant une combinaison de tactiques Meta-F*, d'unification d'ordre supérieur et de SMT.


    Pour avoir un avant-goût de F*, nous allons nous plonger dans quelques exemples. A ce stade, nous ne nous attendons pas à ce que vous compreniez ces exemples en détail, mais cela devrait vous donner un aperçu de ce qui est possible avec F*.


    F* est un langage à typage dépendant

    La programmation typée dépendante permet de capturer plus précisément les propriétés et les invariants d'un programme à l'aide de types. Voici un exemple classique : le type vec a n représente un vecteur à n dimensions d'éléments typés a ; ou, plus simplement, une liste de n valeurs chacune de type a. Comme d'autres langages typés de manière dépendante, F* supporte les définitions inductives de types.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    type vec (a:Type) : nat -> Type =
      | Nil : vec a 0
      | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)
    Les opérations sur les vecteurs peuvent se voir attribuer des types qui décrivent leur comportement en termes de longueur des vecteurs.

    Par exemple, voici une fonction récursive append pour concaténer deux vecteurs. Son type indique que le vecteur résultant a une longueur qui est la somme des longueurs des vecteurs d'entrée.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    let rec append #a #n #m (v1:vec a n) (v2:vec a m)
      : vec a (n + m)
      = match v1 with
        | Nil -> v2
        | Cons hd tl -> Cons hd (append tl v2)
    Bien entendu, une fois qu'une fonction comme append est définie, elle peut être utilisée pour définir d'autres opérations et son type permet de prouver d'autres propriétés. Par exemple, il est facile de montrer que l'inversion d'un vecteur ne modifie pas sa longueur.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    let rec reverse #a #n (v:vec a n)
      : vec a n
      = match v with
        | Nil -> Nil
        | Cons hd tl -> append (reverse tl) (Cons hd Nil)
    Enfin, pour obtenir un élément d'un vecteur, on peut programmer un sélecteur dont le type inclut également un type de raffinement pour spécifier que l'indice i est inférieur à la longueur du vecteur.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    let rec get #a #n (i:nat{i < n}) (v:vec a n)
      : a
      = let Cons hd tl = v in
        if i = 0 then hd
        else get (i - 1) tl
    Bien que des exemples comme celui-ci puissent être programmés dans d'autres langages typés dépendants, ils peuvent souvent être fastidieux, en raison de diverses restrictions techniques. F* fournit une logique de base avec une notion d'égalité plus flexible pour faciliter la programmation et la preuve. Pour l'instant, ce qu'il faut retenir, c'est que les modèles de programmation typés dépendants qui sont assez techniques dans d'autres langages sont souvent assez naturels dans F*.


    F* supporte la programmation avec effet définie par l'utilisateur

    Bien que la programmation fonctionnelle soit au cœur du langage, F* ne se limite pas aux fonctions pures. En fait, F* est un langage complet de Turing. Le fait que cela vaille la peine d'être mentionné peut surprendre les lecteurs ayant une expérience des langages de programmation à usage général tels que C# ou Scala, mais tous les langages typés dépendants ne sont pas complets au sens de Turing, car la non-termination peut rompre la solidité. Cependant, F* supporte les fonctions récursives générales et la non-termination d'une manière sûre, sans compromettre la solidité.

    Au-delà de la non-termination, F* supporte un système d'effets de calcul définis par l'utilisateur qui peuvent être utilisés pour modéliser une variété d'idiomes de programmation, y compris des choses comme l'état mutable, les exceptions, la concurrence, les entrées-sorties, etc.

    Ci-dessous se trouve du code dans un dialecte F* appelé Low* qui fournit un modèle de programmation séquentiel et impératif de type C avec une mémoire mutable. La fonction malloc_copy_free alloue un tableau dest, copie le contenu d'un tableau d'octets src dans dest, désalloue src et renvoie dest.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    let malloc_copy_free (len:uint32 { 0ul < len })
                         (src:lbuffer len uint8)
      : ST (lbuffer len uint8)
           (requires fun h -> 
             live h src /\
             freeable src)
           (ensures fun h0 dest h1 -> 
             live h1 dest /\
             (forall (j:uint32). j < len ==> get h0 src j == get h1 dest j))
      = let dest = malloc 0uy len in
        memcpy len 0ul src dest;
        free src;
        dest
    Il nous faudra attendre bien plus longtemps pour expliquer ce code en détail, mais voici les deux principaux points à retenir :

    • La signature de type de la procédure affirme que, sous certaines contraintes imposées à l'appelant, l'exécution de malloc_copy_free est sûre (par exemple, elle ne lit pas en dehors des limites de la mémoire allouée) et qu'elle est correcte (c'est-à-dire qu'elle copie avec succès src dans dest sans modifier d'autre mémoire).
    • Étant donné l'implémentation d'une procédure, F* construit en fait une preuve mathématique qu'elle est sûre et correcte par rapport à sa signature.


    Bien que d'autres vérificateurs de programmes offrent des fonctionnalités similaires à celles que nous avons utilisées ici, F* se distingue par le fait que la sémantique des programmes avec effets de bord (comme la lecture et l'écriture de la mémoire) est entièrement encodée dans la logique de F* à l'aide d'un système d'effets définis par l'utilisateur.

    Alors que malloc_copy_free est programmé dans Low* et spécifié en utilisant un type particulier de logique Floyd-Hoare, il n'y a rien de vraiment spécial à ce sujet dans F*.

    Voici, par exemple, un programme concurrent dans un autre dialecte F* défini par l'utilisateur et appelé Steel. Il incrémente deux références allouées au tas en parallèle et est spécifié pour la sécurité et la correction dans la logique de séparation concurrente, un type de logique Floyd-Hoare différent de celui que nous avons utilisé pour malloc_copy_free.

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    let par_incr (#v0 #v1:erased int) (r0 r1:ref int)
      : SteelT _ (pts_to r0 v0 `star` pts_to r1 v1)
                 (fun _ -> pts_to r0 (v0 + 1) `star` pts_to r1 (v1 + 1))
      = par (incr r0) (incr r1)
    En tant qu'utilisateur de F*, vous pouvez choisir un modèle de programmation et une suite d'abstractions de preuve de programme pour répondre à vos besoins.

    Source : Introduction du langage F*

    Et vous ?

    Quel est votre avis sur le sujet ?

    Voir aussi :

    La version 5.0.0 d'OCaml, le langage de programmation multi-paradigme est disponible, elle apporte le support du parallélisme en mémoire partagée et les gestionnaires d'effets

    La version 6 de F#, le langage de programmation fonctionnel conçu par Microsoft, est disponible, plus rapide et plus interopérable, elle apporte de nouvelles fonctions

    Faut-il éviter d'utiliser des classes et s'appuyer autant que possible sur une approche fonctionnelle ? Un point de vue d'Andy Peterson basé sur son expérience en entreprise avec Typescript
    Publication de communiqués de presse en informatique. Contribuez au club : corrections, suggestions, critiques, ... Contactez le service news et Rédigez des actualités

  2. #2
    Membre actif
    Profil pro
    DSI
    Inscrit en
    Février 2010
    Messages
    85
    Détails du profil
    Informations personnelles :
    Localisation : France, Paris (Île de France)

    Informations professionnelles :
    Activité : DSI

    Informations forums :
    Inscription : Février 2010
    Messages : 85
    Points : 287
    Points
    287
    Par défaut
    "F*" ils n'ont pas pu trouver un autre nom pour ce langage ?
    et le version superirur sera F*** ?

Discussions similaires

  1. Réponses: 0
    Dernier message: 10/05/2024, 16h08
  2. Réponses: 0
    Dernier message: 14/04/2020, 14h16
  3. [Questions]Le langage de programmation Binaire existe t-il ?
    Par Nasky dans le forum Langages de programmation
    Réponses: 30
    Dernier message: 16/11/2012, 09h09
  4. Création d'un langage de programmation
    Par liquid_stone dans le forum Langages de programmation
    Réponses: 5
    Dernier message: 09/11/2003, 16h44
  5. Nombre de langage de programmation total
    Par Adrael dans le forum Langages de programmation
    Réponses: 16
    Dernier message: 22/07/2003, 00h06

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo