Accueil🇫🇷Chercher

Anubis (langage)

Anubis est un langage de programmation informatique. C'est un langage fonctionnel avec type créé en 2000 par le mathématicien français Alain Prouté en se basant sur une partie de mathématiques au sein de la logique, nommée la théorie des catégories.

Description

Par construction basée sur les mathématiques, ce langage nous donne une capacité de programmation sure (au sens de programmes démontrables).

Le principe de la construction du langage Anubis est de définir chaque élément du langage au moyen de la théorie des catégories bicartésiennes fermées. L'objectif est d'obtenir un langage sûr, facilitant l'écriture de démonstrations de correction de programmes à la manière d'un assistant de preuve.

Parmi les Ă©lĂ©ments qui contribuent Ă  cette sĂ»retĂ© de fonctionnement du programme Ă  son exĂ©cution, figurent le branchement conditionnel d'Anubis, qui oblige le programmeur Ă  traiter tous les cas possibles, et l'absence d'exceptions. Cette dernière, la conditionnelle ainsi formulĂ©e, oblige le programmeur Ă  tenir compte de tous les rĂ©sultats possibles d'une opĂ©ration. Ainsi, par exemple, la division d'entiers peut renvoyer un entier ou une valeur indiquant l'absence de rĂ©sultat, car la division par zĂ©ro provoque une erreur.

Exemple de programme

Il s'agit de calculer la longueur d'une liste. D'abord, le type des listes est défini comme suit :

type List($T):
   [ ], 
   [$T . List($T)].

Dans cette définition, $T représente un type quelconque. Ceci est donc un « schéma » de définition de type. Le type a deux variantes (deuxième et troisième ligne de la définition), qui représentent respectivement la liste vide et les listes non vides.

Le calcul de la longueur d'une liste oblige à détruire la donnée de type List($T) qui est fournie. Ceci est réalisé obligatoirement avec une conditionnelle :

define Int32 length(List($T) l) =
   if l is 
     {
        [ ]           then 0, 
        [head . tail] then 1 + length(tail)
     }.

Ce qui différencie fondamentalement Anubis des langages de la famille ML est le fait qu'une telle conditionnelle ne constitue pas un filtre car il est obligatoire de prévoir un unique traitement par cas possible. Ainsi, il n'y a pas de problème lié à l'ordre des filtres, et il n'y a jamais d'exception lancée au cas où aucun filtre ne conviendrait. Il y a donc saut direct au cas concerné, sans essais successifs. Ce comportement est la traduction exacte du problème universel qui définit les sommes en théorie des catégories, alors que le filtrage modélise une union non nécessairement disjointe et ne couvrant pas nécessairement tous les cas possibles. Cette caractéristique du langage Anubis est une source essentielle de sûreté et de facilité de maintenance des programmes.

Autres caractéristiques

Anubis est un langage à vocation universelle. Il autorise l'utilisation de constructions impératives (tout en recommandant de les limiter au strict nécessaire), ainsi que la programmation orientée objet. Il est nécessaire de montrer comment il se comporte et combien il est à l'aise avec tous les styles (on parle souvent abusivement de 'paradigmes' de développement) du type (TDD, BDD (Test, Type, Behaviour) Driven Development).

Critiques

Si les constructions d'Anubis garantissent la sûreté, c'est au prix de programmes longs car ils doivent traiter tous les cas possibles, même lorsque l'on peut démontrer qu'ils ne peuvent pas se produire. Par exemple, écrire x/2 oblige à traiter le cas de la division par zéro alors que 2 est différent de zéro.

Voir aussi

Articles connexes

  • Charity, un autre langage de programmation fondĂ© sur la thĂ©orie des catĂ©gories.

Liens externes

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.