ATS (langage de programmation)
From Wikipedia, the free encyclopedia
La mise en forme de cet article est à améliorer ().
La mise en forme du texte ne suit pas les recommandations de Wikipédia : il faut le « wikifier ».
Les points d'amélioration suivants sont les cas les plus fréquents :
- Les titres sont pré-formatés par le logiciel. Ils ne sont ni en capitales, ni en gras.
- Le texte ne doit pas être écrit en capitales (les noms de famille non plus), ni en gras, ni en italique, ni en « petit »…
- Le gras n'est utilisé que pour surligner le titre de l'article dans l'introduction, une seule fois.
- L'italique est rarement utilisé : mots en langue étrangère, titres d'œuvres, noms de bateaux, etc.
- Les citations ne sont pas en italique mais en corps de texte normal. Elles sont entourées par des guillemets français : « et ».
- Les listes à puces sont à éviter, des paragraphes rédigés étant largement préférés. Les tableaux sont à réserver à la présentation de données structurées (résultats, etc.).
- Les appels de note de bas de page (petits chiffres en exposant, introduits par l'outil «
Source - Les liens internes (vers d'autres articles de Wikipédia) sont à choisir avec parcimonie. Créez des liens vers des articles approfondissant le sujet. Les termes génériques sans rapport avec le sujet sont à éviter, ainsi que les répétitions de liens vers un même terme.
- Les liens externes sont à placer uniquement dans une section « Liens externes », à la fin de l'article. Ces liens sont à choisir avec parcimonie suivant les règles définies. Si un lien sert de source à l'article, son insertion dans le texte est à faire par les notes de bas de page.
- La présentation des références doit suivre les conventions bibliographiques. Il est recommandé d'utiliser les modèles {{Ouvrage}}, {{Chapitre}}, {{Article}}, {{Lien web}} et/ou {{Bibliographie}}. Le mode d'édition visuel peut mettre en forme automatiquement les références.
- Insérer une infobox (cadre d'informations à droite) n'est pas obligatoire pour parachever la mise en page.
Pour une aide détaillée, merci de consulter Aide:Wikification.
Si vous pensez que ces points ont été résolus, vous pouvez retirer ce bandeau et améliorer la mise en forme d'un autre article.
L'article doit être débarrassé d'une partie de son jargon ().
Sa qualité peut être largement améliorée en utilisant un vocabulaire plus directement compréhensible.
Discutez des points à améliorer en page de discussion.
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?ATS (Applied Type System) est un langage de programmation conçu pour unifier la programmation avec des spécifications formelles. ATS prend en charge la combinaison de la démonstration du théorème avec la programmation pratique grâce à l'utilisation de systèmes de type avancés[1]. Une version antérieure de The Computer Language Benchmarks Game a démontré que les performances d'ATS sont comparables à celles des langages de programmation C et C++[2]. En utilisant la preuve de théorème et la vérification de type stricte, le compilateur peut détecter et prouver que ses fonctions implémentées ne sont pas sensibles aux bogues tels que la division par zéro, les fuites de mémoire, le dépassement de mémoire tampon et d'autres formes de corruption de mémoire en vérifiant l' arithmétique du pointeur et le comptage de références avant que le programme se compile. De plus, en utilisant le système de démonstration de théorème intégré de l'ATS (ATS / LF), le programmeur peut utiliser des constructions statiques qui sont entrelacées avec le code opérationnel pour prouver qu'une fonction atteint sa spécification.
ATS est principalement dérivé des langages de programmation ML et OCaml. Une langue antérieure, Dependent ML, du même auteur a été incorporée par la langue.
La dernière version d'ATS1 (Anairiats) est sortie en v0.2.12 le 20/01/2015[3]. La première version d'ATS2 (Postiats) est sortie en septembre 2013 [4]
Preuve du théorème
L'objectif principal de l'ATS est de soutenir la démonstration de théorèmes en combinaison avec une programmation pratique[1]. Avec la démonstration d'un théorème, on peut prouver, par exemple, qu'une fonction implémentée ne produit pas de fuites de mémoire. Cela évite également d'autres bogues qui, autrement, ne pourraient être trouvés que pendant les tests. Il incorpore un système similaire à ceux des assistants de preuve qui visent généralement uniquement à vérifier les preuves mathématiques, sauf que ATS utilise cette capacité pour prouver que les implémentations de ses fonctions fonctionnent correctement et produisent le résultat attendu.
À titre d'exemple simple, dans une fonction utilisant la division, le programmeur peut prouver que le diviseur ne sera jamais égal à zéro, empêchant une Division par zéro. Disons que le diviseur «X» a été calculé comme 5 fois la longueur de la liste «A». On peut prouver que dans le cas d'une liste non vide, «X» est non nul, puisque «X» est le produit de deux nombres non nuls (5 et la longueur de «A»). Un exemple plus pratique serait de prouver par le comptage de références que le compte de rétention sur un bloc de mémoire alloué est correctement compté pour chaque pointeur. On peut alors savoir, et prouver littéralement, que l'objet ne sera pas désalloué prématurément, et que les fuites de mémoire ne se produiront pas.
L'avantage du système ATS est que puisque toute démonstration de théorème se produit strictement dans le compilateur, cela n'a aucun effet sur la vitesse du programme exécutable. Le code ATS est souvent plus difficile à compiler que le code C standard, mais une fois qu'il est compilé, le programmeur peut être certain qu'il s'exécute correctement au degré spécifié par leurs preuves (en supposant que le compilateur et le système d'exécution sont corrects).
Dans ATS, les preuves sont distinctes de l'implémentation, il est donc possible d'implémenter une fonction sans la prouver si le programmeur le souhaite.
Représentation des données
Selon l'auteur (Hongwei Xi), l'efficacité d'ATS [5] est en grande partie due à la façon dont les données sont représentées dans le langage et aux optimisations de fin d'appel (qui sont généralement importantes pour l'efficacité des langages de programmation fonctionnels). Les données peuvent être stockées dans une représentation plate ou non encadrée plutôt que dans une représentation encadrée.
