Anubis (langage)
Anubis est un langage de programmation informatique. C'est un langage fonctionnel avec type créé en 2000 par le mathématicien congolais 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[modifier]
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[modifier]
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[modifier]
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[modifier]
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[modifier]
Articles connexes[modifier]
- Charity, un autre langage de programmation fondé sur la théorie des catégories.
Liens externes[modifier]
Erreur Lua dans Module:Catégorisation_badges à la ligne 170 : attempt to index field 'wikibase' (a nil value).Erreur Lua dans Module:Suivi_des_biographies à la ligne 189 : attempt to index field 'wikibase' (a nil value).
Cet Article wiki "Anubis (langage)" est issu de Wikipedia. La liste de ses auteurs peut être visible dans ses historiques et/ou la page Edithistory:Anubis (langage).
