Aller au contenu

ATS (langage de programmation)

Un article de Wikipédia, l'encyclopédie libre.

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

[modifier | modifier le code]

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

[modifier | modifier le code]

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.

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

[modifier | modifier le code]

Propositions

[modifier | modifier le code]

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 » :

 FACT(n, r) ssi fact(n) = r
 MUL(n, m, prod) ssi n * m = prod
 
 FACT(n, r) = 
     FACT(0, 1) 
   | FACT(n, r) ssi FACT(n-1, r1) et MUL(n, r1, r) // pour n> 0
 
 // exprime le fact(n) = r ssi r = n * r1 et r1 = fact(n-1)

En code ATS :

 dataprop FACT (int, int) =
  | FACTbas (0, 1)       // basic case: FACT(0, 1)
  | {n:int | n > 0} {r,r1:int} // inductive case
    FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))

où FACT (int, int) est un type de preuve

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)

[modifier | modifier le code]
[FACT (n, r)] implique [fact (n) = r]
 [MUL (n, m, prod)] implique [n * m = prod]
FAIT (0, 1)
 FACT (n, r) ssi FACT (n-1, r1) et MUL (n, r1, r) pour tout n> 0

Se souvenir:

{...} quantification universelle
[...] quantification existentielle
(... | ...) (preuve | valeur)
@ (...) tuple plat ou tuple de paramètres de fonction variadique
. <...>. métrique de terminaison [6]
#include "share/atspre_staload.hats"

dataprop FACT (int, int) =
 | FACTbas (0, 1) of () // basic case
 | {n:nat}{r:int}    // inductive case
  FACTind (n+1, (n+1)*r) of (FACT (n, r))

(* note that int(x), also int x, is the monovalued type of the int x value.

 The function signature below says:
 forall n:nat, exists r:int where fact( num: int(n)) returns (FACT (n, r) | int(r)) *)

fun fact{n:nat} .<n>. (n: int (n)) : [r:int] (FACT (n, r) | int(r)) =
(
 ifcase
 | n > 0 => ((FACTind(pf1) | n * r1)) where 
 { 
  val (pf1 | r1) = fact (n-1)
 }
 | _(*else*) => (FACTbas() | 1)
)

Partie 2 (routines et test)

[modifier | modifier le code]
implement main0 (argc, argv) =
{
 val () = if (argc != 2) then prerrln! ("Usage: ", argv[0], " <integer>")

 val () = assert (argc >= 2)
 val n0 = g0string2int (argv[1])
 val n0 = g1ofg0 (n0)
 val () = assert (n0 >= 0)
 val (_(*pf*) | res) = fact (n0)

 val ((*void*)) = println! ("fact(", n0, ") = ", res)
}

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)

$ patscc fact1.dats -o fact1
$ ./fact1 4

compile et donne le résultat attendu

Types de base

[modifier | modifier le code]
  • 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

[modifier | modifier le code]
préfixe @ ou aucun signifie allocation directe, plate ou sans boîte
 val x : @(int, char) = @(15, 'c') // x.0 = 15 ; x.1 = 'c'
 val @(a, b) = x          // pattern matching binding, a= 15, b='c'
 val x = @{first=15, second='c'}  // x.first = 15
 val @{first=a, second=b} = x    // a= 15, b='c'
 val @{second=b, ...} = x      // with omission, b='c'
préfixe 'signifie allocation indirecte ou encadrée
 val x : '(int, char) = '(15, 'c') // x.0 = 15 ; x.1 = 'c'
 val '(a, b) = x          // a= 15, b='c'
 val x = '{first=15, second='c'}  // x.first = 15
 val '{first=a, second=b} = x    // a= 15, b='c'
 val '{second=b, ...} = x      // b='c'
spécial

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

val (predicate_proofs | values) = mes paramètres
{...} quantification universelle
[...] quantification existentielle
(...) expression entre parenthèses ou tuple

(... | ...) (preuves | valeurs)
. <...>. métrique de terminaison

@ (...) tuple plat ou tuple de paramètres de fonction variadique (voir l'exemple printf)

@ [byte] [BUFLEN] type d'un tableau de valeurs BUFLEN de type octet 
@ [byte] [BUFLEN] () instance de tableau
@ [byte] [BUFLEN] (0) tableau initialisé à 0

dictionnaire

[modifier | modifier le code]
sorte
domaine
 sortdef nat = {a: int | a >= 0 }   // from prelude:  ''a''  int ...

 typedef String = [a:nat] string(a)  // [..]:  ''a''  nat ...
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" [7].
taper
version linéaire du type précédent avec longueur abstraite. Également des types non emballés[7].
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
 fun {a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): @(a @ l | a)
 
 fun {a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): @(a @ l | void)
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 [8]
viewdef array_v (a: viewt @ ype, n: int, l: addr) = @ [a] [n] @ l
T?
type éventuellement non initialisé

l'exhaustivité de la correspondance des modèles

[modifier | modifier le code]

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é
 staload "foo.sats" // foo.sats is loaded and then opened into the current namespace

 staload F = "foo.sats" // to use identifiers qualified as $F.bar

 dynload "foo.dats" // loaded dynamically at run-time

vue de données

[modifier | modifier le code]

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

[modifier | modifier le code]

Types de données

type de données jour ouvrable = Mon | Tue | Mer | Thu | ven

listes

type de données list0 (a: t @ ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)

dataviewtype

[modifier | modifier le code]

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[9].

variables locales

var res: int avec pf_res = 1 // introduit pf_res comme alias de view @ (res)

sur l' allocation de tableau de pile:

#define BUFLEN 10
var! p_buf avec pf_buf = @ [octet] [BUFLEN] (0) // pf_buf = @ [octet] [BUFLEN] (0) @ p_buf 

Voir les déclarations val et var

Références

[modifier | modifier le code]

Liens externes

[modifier | modifier le code]