# ATS (langage de programmation)

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. 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++. 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.

## Histoire

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. La première version d'ATS2 (Postiats) est sortie en septembre 2013

## 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. 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 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.

## Preuve du théorème: un cas d'introduction
### Propositions

dataprop exprime les prédicats sous forme de types algébriques.
Exemple de prédicats en pseudo-code assez similaire à la source ATS (voir ci-dessous pour une source ATS valide) pour la fonction factorielle, dont le nom est abrégé en « FACT » :
En code ATS :
où FACT (int, int) est un type de preuve

### Exemple

Factoriel non récursif avec proposition ou " Théorème " prouvant à travers la construction dataprop.
L'évaluation de fact1 (n-1) renvoie une paire (proof_n_minus_1 | result_of_n_minus_1) qui est utilisée dans le calcul de fact1 (n). Les preuves expriment les prédicats de la proposition.

#### Partie 1 (algorithme et propositions)

Se souvenir:

#### Partie 2 (routines et test)

Tout cela peut être ajouté à un seul fichier et compilé comme suit. La compilation devrait fonctionner avec divers compilateurs C back-end, par exemple gcc . Le nettoyage de la mémoire n'est pas utilisé sauf indication explicite avec -D_ATS_GCATS)
compile et donne le résultat attendu

### Types de base

* booléen (vrai, faux)
* int (littéraux: 255, 0377, 0xFF), unaire moins comme ~ (comme dans ML)
* double
* char 'a'
* chaîne "abc"

### Tuples et disques
#### spécial

Avec '|' comme séparateur, certaines fonctions renvoient la valeur du résultat encapsulée avec une évaluation des prédicats

### dictionnaire
#### sorte

    domaine

#### type (comme tri)

    tri générique pour les éléments de la longueur d'un mot pointeur, à utiliser dans les fonctions polymorphes paramétrées par type. Également "types en boîte".

#### taper

    version linéaire du type précédent avec longueur abstraite. Également des types non emballés.

#### viewtype

    une classe de domaine comme type avec une vue (association de mémoire)

#### viewt @ ype

    version linéaire du type de vue avec une longueur abstraite. Il remplace le type de vue

#### vue

    relation d'un Type et d'un emplacement mémoire. L'infixe @ est son constructeur le plus courant
    T @ L affirme qu'il existe une vue de type T à l'emplacement L
    le type de ptr_get0 (T) est ∀ l : adr. (T @ l | ptr (l)) → (T @ l | T) // voir manuel, section 7.1. Accès sécurisé à la mémoire via des pointeurs

#### T?

    type éventuellement non initialisé

### l'exhaustivité de la correspondance des modèles

comme dans le cas +, val +, type +, viewtype +,. . .
* avec le suffixe '+' le compilateur émet une erreur en cas d'alternatives non exhaustives
* sans suffixe, le compilateur émet un avertissement
* avec '-' comme suffixe, évite le contrôle d'exhaustivité

### vue de données

Les vues de données sont souvent déclarées pour encoder des relations définies de manière récursive sur des ressources linéaires.
dataview array_v (a: viewt @ ype +, int, addr) = | {l: addr} array_v_none (a, 0, l) | {n: nat} {l: addr} array_v_some (a, n + 1, l) of (a @ l, array_v (a, n, l + sizeof a))

### type de données / type de vue de données

Types de données
listes

#### dataviewtype

Un type de vue de données est similaire à un type de données, mais il est linéaire. Avec un dataviewtype, le programmeur est autorisé à libérer explicitement (ou désallouer) de manière sûre la mémoire utilisée pour stocker les constructeurs associés au dataviewtype.

### variables

variables locales
sur l' allocation de tableau de pile:
Voir les déclarations val et var