Langage Anubis

Langage Anubis

Anubis (langage)

Anubis est un langage fonctionnel créé en 2000 par le mathématicien français Alain Prouté en se basant sur la théorie des catégories.

Sommaire

Description

Le principe de la construction d'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é figurent le branchement conditionnel d'Anubis, qui oblige le programmeur à traiter tous les cas possibles, et l'absence d'exceptions. Cette dernière oblige le programmeur à tenir compte de tous les résultats possibles d'une opération. Ainsi, 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 « alternatives » (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 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.

Anubis 2

La deuxième version d'Anubis est en préparation. Basée sur des catégories particulières appelées topos, elle sera plus proche d'un assistant de preuve.

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

  • (en) Charity, un autre langage de programmation fondé sur la théorie des catégories.

Liens externes

  • Portail de la programmation informatique Portail de la programmation informatique
Ce document provient de « Anubis (langage) ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Langage Anubis de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

  • Anubis (langage) — Anubis est un langage fonctionnel créé en 2000 par le mathématicien français Alain Prouté en se basant sur la théorie des catégories. Sommaire 1 Description 2 Exemple de programme 3 Autres caractéristiques …   Wikipédia en Français

  • Anubis (Homonymie) — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Anubis : dieu de la mythologie égyptienne Anubis : personnage fictif de la série télévisée Stargate SG 1 Anubis : langage de programmation… …   Wikipédia en Français

  • Langage fonctionnel — Programmation fonctionnelle La programmation fonctionnelle est un paradigme de programmation qui considère le calcul en tant qu évaluation de fonctions mathématiques et rejette le changement d état et la mutation des données. Elle souligne l… …   Wikipédia en Français

  • Anubis (homonymie) — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Anubis : dieu de la mythologie égyptienne Anubis : personnage fictif de la série télévisée Stargate SG 1 Anubis : langage de programmation… …   Wikipédia en Français

  • Programmation fonctionnelle — La programmation fonctionnelle est un paradigme de programmation qui considère le calcul en tant qu évaluation de fonctions mathématiques et rejette le changement d état et la mutation des données. Elle souligne l application des fonctions,… …   Wikipédia en Français

  • Planetes de Stargate — Planètes de Stargate Cette page répertorie les planètes du monde de Stargate. Dans Stargate SG 1, les équipes accomplissent leurs missions dans notre galaxie, qui est une galaxie spirale du groupe local. Dans Stargate Atlantis, les équipes… …   Wikipédia en Français

  • Planète de Stargate — Planètes de Stargate Cette page répertorie les planètes du monde de Stargate. Dans Stargate SG 1, les équipes accomplissent leurs missions dans notre galaxie, qui est une galaxie spirale du groupe local. Dans Stargate Atlantis, les équipes… …   Wikipédia en Français

  • Planètes de stargate — Cette page répertorie les planètes du monde de Stargate. Dans Stargate SG 1, les équipes accomplissent leurs missions dans notre galaxie, qui est une galaxie spirale du groupe local. Dans Stargate Atlantis, les équipes accomplissent leurs… …   Wikipédia en Français

  • Vorash — Planètes de Stargate Cette page répertorie les planètes du monde de Stargate. Dans Stargate SG 1, les équipes accomplissent leurs missions dans notre galaxie, qui est une galaxie spirale du groupe local. Dans Stargate Atlantis, les équipes… …   Wikipédia en Français

  • Recit originel — Récit originel Création du monde par Odin et ses frères de Lorenz Frølich Un récit originel est une explication, scientifique ou mythologique, des débuts de l humanité, la terre, la vie et l univers (cosmogonie). C …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”