Xanadu: Imperative Programming with Dependent Types [Romanian]

Original in English by Hongwei Xi

Xanadu: programare imperativă cu tipuri dependente


Noi propunem o îmbogăţire a a programării imperative practice cu un tip de disciplină, care permite specificarea şi amestecarea de informaţii mult mai precise cu privire la programele, decât cele aplicate în limbi, cum ar fi Java şi Standard ML (SML).

Motivaţia principală pentru dezvoltarea unui astfel de tip de disciplină este de permite programatorului să-şi exprime mai multe proprietăţi de program cu aceste tipuri şi de a implementa aceste proprietăţi prin intermediul verificării de tip. Este bine cunoscut faptul că un tip de disciplină, cum ar fi cel aplicat în Java sau SLM, poate facilita în mod eficient detectarea erorilor de program. Prin urmare, se poate de aşteptat că o disciplină de tip puternic poate ajuta la detectarea mai multor erori de program, care o să conducă la producerea software-ului mult mai robust.

În linii generale, există două direcţii de extindere a unui stil a tipului de sistem lui Hindley-Milner, cum ar fi acel din SML.Una este de a extinde stilul, astfel încât mai multe programe să poată să fie admise ca tip corect, şi cealaltă este de a se extinde, astfel încât programele să poată să fie atribuite la mai multe tipuri precise. Suntem în primul rând interesaâi în această direcţie din urmă.

Noţiunea de tipuri dependente, care a fost în mare parte inventată pentru modelarea programelor cu mai multă acurateţe, a fost studiată timp de cel puţin trei decenii. Cu toate acestea, utilizarea tipurilor dependente în practică de programare a fost foarte rară în cazul în care existau, şi aceasta, credem noi, a fsot în general cauzat de unele dificultăţi mari în proiectarea unui algoritm de inferenţă practic şi util pentru un sistem de tip dependent. Noi am prezentat o abordare la soluţionarea dificultăţilor în proiectarea de ML dependent (DLM), care extinde ML, cu o noţiune de formă restrânsă a tipurilor dependente. De asemenea, este demonstrat faptul că tipuri dependente în DLM pot facilita de eliminarea controlului matricelui legat, eliminarea verificării etichetei şi reprezentare tipurilor de date fără etichete. Evident, o întrebare imediată este dacă putem culege unele beneficii similare, prin incorporarea tipurilor dependente în programare imperativă. Noi propunem să abordăm această problemă prin proiectarea unui limbaj de programare imperativă dependentă de tip.

Există şi altă motivaţie pentru a integra tipuri dependente în programare practică. Într-un mediu de programare fără încredere, cum ar fi Internet, codul mobil primit de la o sursă necunoscută nu poate fi de încredere. Prin urmare, destinatarul codului des trebuie să efectueze anumite verificări statice şi/sau dinamice de pe codul mobil primit pentru a preveni o consecinţă nedorită, cum ar fi o breşă de securitate. Noi am creat un limbaj de asamblare dependent de tip (DTAL, de la eng. dependently typed assembly language), în care sistemul de tip poate garanta siguranţa de memorie a codului DTAL, în cazul în care siguranţa de memorie constă în tipul de siguranţă, cât şi în subscripting-ul matricelui în condiţii de siguranţă. Este, totuşi, dificil de a compila în cod DTAL un program scris într-o limbă, cum ar fi, de exemplu, Java, deoarece se pare des ineficient pentru a sintetiza de la un astfel de program de tipul de informaţii necesare în codul DTAL. Cu un limbaj de programare imperativ dependent tastat, noi avfem să implementăm un compilator care poate traduce tipuri dependente, la nivel de sursă în tipuri dependente, la nivel de asamblare, producînd cod DTAL eficient.

Pe scurt, noi propunem să proiectăm un limbaj de programare imperativă dependentă de tip pentru studierea utilizării de tipuri dependente în programare imperativă practică la nivel de sursă, cât şi la nivel de asamblare. Noi aşteptăm că acest studiu poate duce la producerea software-ului, care va fi nu numai mai robust, dar, de asemenea, mai puţin costisitor pentru menţinere.

  • Ce este Xanadu?

    Xanadu este un limbaj de programare imperativă dependent tastată. Aici este o scurtă introducere (ppt)

  • Exemple de programe în Xanadu:

    Vă prezentăm câteva exemple realiste în Xanadu pentru sprijinul practic de Xanadu.

    • Căutare binară:

      Următoarea este o implementare a căutării binare pe un matrice întreg în Xanadu. Noutatea în implemenare constă în adnotarea după cuvinte cheie invariante. Această adnotare este un tip dependent, care susţine unele informaţii de la punctul de intrare a buclei. În acest caz, stările adnotării pe care variabilele scăyute şi înalte au tastat sunt int (i) şi int (j) la punctul de intrare pentru anumite numere întregi i şi j, astfel încât atât deţin 0 <= i <= n cît şi 0 <= j + 1 <= n. Acesta este o buclă invariantă, care poate garanta subscriptingul matricelui operationvec [mid], şi în corpul buclei este sigur, astfel încît, nu poate ieşi din limite. Punctul crucial este acea verificare de tip în Xanadu care poate verifica automat dacă un program este invariant ca aceasta, care este furnizat de programator, este într-adevăr un program corect invariant.

      În plus, în mod automat, de asemenea, în Xanadu se verifică dacă o variabilă este deja iniţializată înainte de a fi citit.

      {n:nat}
      int bsearch(key: int, vec[n]: int) {
        var: int low, mid, high;
             int x;;
      
        low = 0; high = arraysize(vec) - 1;
      
        invariant:
          [i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
        while (low <= high) {
          mid = (low + high) / 2;
          x = vec[mid];
          if (key == x) { return mid; }
          else if (key < x) { high = mid - 1; }
               else { low = mid + 1; }
        }
        return -1;
      }
    • Lista inversă:

      Acest exemplu demonstrează că aceasta poate fi verificată în sistemul de tip de Xanadu co o funcţie de listă inversă care este lungimea de conservare.

      Următoarea declaraţie declară un tip de uniune polimorf de listă <'a>. Cei doi constructori Nil şi conservator asociate cu tipul de uniune sunt tipurile date de lista <'a> (0) şi {n:nat} 'a * <'a> lista (n) -> <'a> lista(n+1), respectiv, ceea ce înseamnă că zero este o listă de lungime 0 şi conservatori returnează o listă de lungime n +! atunci când se administrează un element şi o listă de lungime n. Reţineţi că {n:nat} indică faptul că n, este un indice variabil de tip nat, care este universal cuantificat. nat este un indice de tip, care reprezintă un număr natural.

      union <'a> list with nat {
       Nil(0);
       {n:nat} Cons(n+1) of 'a * <'a> list(n)
      }

      Următorul implementează funcţia de adăugare inversă pe liste.Antetul a stărilor de funcţii care pentru numere naturale m şi n, rev_app ia o pereche de liste de lungime m şi n şi returnează o listă de lungime m + n. Este clar că iese, ceea ce înseamnă că un program se opreşte anormal, şi nu poate fi niciodată executat la timpul de rulare şi, prin urmare, este inutil în acest caz. Din păcate, aceste informaţii nu pot fi captate în sistemul de tip Xanadu.

      ('a){m:nat, n:nat}
      <'a> list(m+n) rev_app
       (xs: <'a> list(m), ys: <'a> list(n)) {
         var: 'a x;;
        
         invariant:
           [m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1))
         while (true) {
           switch (xs) {
             case Nil: return ys;
             case Cons(x, xs): ys = Cons(x, ys);
           }
         }
         exit;
      }

      Funcţia listei inverse poate fi acum pusă în aplicare după cum urmează.Antet al funcţiei indică faptul că aceasta este o funcţie conservare a lungimii.

      ('a){n:nat}
      <'a> list(n) reverse (xs: <'a> list(n)) {
         return rev_app (xs, Nil);
      }
    • Înmulţirea matricelui împrăştiat:

      Noi implementăm multiplicarea între matrice rar şi un vector. Vom defini o înregistrare polimorfică a matricelui împrăştiat <'a> pentru a reprezenta două tablouri tridimensionale rare, în care fiecare element este de tip 'a. Matricele împrăştiat <'a> este indexat cu o pereche de numere naturale (m, n), care înseamnă numărul de rânduri şi numărul de coloane dintr-o matrice rară, respectiv. Să rpesupunem că sa este o înregistrare a tipului a matricelui împrăştiat <'a> (m, n). Astfel, sa are trei componente, şi anume, de rând, coloană şi de date. În mod evident, tipurile atribuite la rând şi coloană indică că sa ţi sa.col se întorc la dimensiunile de tip sa atribuit de date ce prevede că sa.data este o matrice de dimensiune m. În această matrice, fiecare element, care reprezintă un rând într-o matrice rară, este o listă de perechi şi fiecare pereche constă dintr-un număr natural mai mic decât n şi un element de tip 'a.

      {m:nat,n:nat}
      record <'a> sparseArray(m, n) {
        row: int(m);
        col: int(n);
        data[m]: <int[0,n) * 'a> list
      }

      Functie mat_vec_mult are un matrice împrăştiat cu puctul plutitor de dimensiune (m, n) şi un punct plutitor de vector de dimensiune n de dimensiune m. Reţineţi că funcţia list_vec_mult este utilizată pentru calculul produsului punctului rândului în matrice împrăştiate şi vector. Punctul pe care noi facem este acel de tip de sistem Xanadu care poate garanta toate operaţiunile subscripting-ului de matrice, în acest exemplu pentru a fi în siguranţă în timpul rulării.

      {n:nat}
      float
      list_vec_mult (xs: <int[0,n) * float> list, vec[n]: float) {
        var: int i; float f, sum;;
      
        sum = 0.0;
        while (true) {
          switch (xs) {
            case Nil: return sum;
            case Cons((i, f), xs): sum = sum +. f *. vec[i];      
          }
        }
        exit;    
      }
      
      {m:nat,n:nat}
      <float> array(m)
      mat_vec_mult(mat: <float> sparseArray(m, n), vec[n]: float) {
        var: nat i; float result[];;
      
        result = newarray(mat.row, 0.0);
      
        for (i = 0; i < mat.row; i = i + 1) {
          result[i] = list_vec_mult (mat.data[i], vec);
        }
        return result;
      }
    • Sortare de masive:

      Ar putea să îţi dai seama asta de unul singur :-)

      {max:nat}
      record <'a> heap(max) {
        max: int(max);
        mutable size: [size:nat | size <= max] int(size);
        data[max]: 'a
      }
      
      {max:nat, i:nat | i < max}
      unit heapify (heap: <float> heap(max), i: int(i)) {
        var: int size, left, right;
             float temp;
             largest: [a:nat | a < max] int(a) ;;
      
        left = 2 * i + 1; right = 2 * i + 2;
      
        size = heap.size; largest = i;
      
        if (left < size) {
          if (heap.data[left] >. heap.data[i]) { largest = left; }
        }
      
        if (right < size) {
          if (heap.data[right] >. heap.data[largest]) { largest = right; }
        }
      
        if (largest <> i) {
          temp = heap.data[i];
          heap.data[i] = heap.data[largest];
          heap.data[largest] = temp;
          heapify (heap, largest);
        }
      }
      
      {max:nat}
      unit buildheap (heap: <float> heap(max)) {
        var: int i, size;;
       
        size = heap.size;
       
        invariant: [i:int | i < max] (i: int(i))
        for (i =  size / 2 - 1; i >= 0; i = i - 1) {
          heapify (heap, i);
        }
      }
      
      {max:nat}
      unit heapsort (heap: <float> heap(max)) {
        var: int size, i; float temp;;
      
        buildheap (heap);
        invariant: [i:int | i < max] (i: int(i))
        for (i = heap.max - 1; i >= 1; i = i - 1) {
          temp = heap.data[i];
          heap.data[i] = heap.data[0];
          heap.data[0] = temp;
          heap.size = i;
          heapify(heap, 0);
        }
      }
      
      
    • Eliminarea Gaussiană:

      Aţi putea să va daţi seama de asta de sinestătător

      {m:nat, n:nat}
      record <'a> matrix(m,n) {
        row: int(m);
        col: int(n);
        data[m][n]: 'a
      }
      
      {m:nat,n:nat,i:nat,j:nat | i < m, j < m}
      unit
      rowSwap(data[m][n]: float, i:int(i), j:int(j)) {
        var: temp[]: float;;
        temp = data[i];
        data[i] = data[j];
        data[j] = temp;
      }
      
      {n:nat,i:nat | i < n}
      unit
      norm(r[n]: float, n:int(n), i:int(i)) {
        var: float x;;
      
        x = r[i]; r[i] = 1.0; i = i + 1;
      
        invariant: [i:nat] (i: int(i))
        while (i < n) { r[i] = r[i] /. x; i = i + 1;}
      }
      
      {n:nat, i:nat | i < n}
      unit
      rowElim(r[n]: float, s[n]: float, n:int(n), i: int(i)) {
        var: float x;;
      
        x = s[i]; s[i] = 0.0; i = i + 1;
      
        invariant: [i:nat] (i: int(i))
        while (i < n) { s[i] = s[i] -. x *. r[i]; i = i + 1;}
      }
      
      {m:nat, n:nat, i:nat | m > i, n > i}
      [k:nat | k < m] int(k)
      rowMax (data[m][n]: float, m: int(m), i: int(i)) {
        var: nat j; float x, y;
             max: [k: nat | k < m] int(k);;
      
        max = i; x = fabs(data[i][i]); j = i + 1;
        
        while (j < m) {
          y = fabs(data[j][i]);
          if (y >. x) { x = y; max = j; }
          j = j + 1;
        }
        return max;
      }
      
      {n:nat | n > 0}
      unit gauss (mat: <float> matrix(n,n+1)) {
        var: float data[][n+1]; nat i, j, max, n;;
      
        data = mat.data; n = mat.row;
        for (i = 0; i < n; i = i + 1) {
          max = rowMax(data, n, i);
          norm (data[max], n+1, i);
          rowSwap(data, i, max);
          for (j = i + 1; j < n; j = j + 1) {
            rowElim(data[i], data[j], n+1, i);
          }
        }
      }
    • Mai multe exemple:

      Vă rugăm să găsiţi mai multe şi mai mari exemple aici – here.

  • Documentele despre Xanadu

    • Hongwe Xi, Facilitating Program Verification with Dependent Types, December 1999. (draft)
    • Hongwe Xi, Imperative Programming with Dependent Types, December 1999. (draft) (extended abstract)
    • Hongwei Xi and Robert Harper, A Dependently Typed Assembly Language, Technical report OGI-CSE-99-008, July 1999. (bibtex) (ps) (pdf) (extended abstract)
  • Diapozitive

    O discuţie dspre Xanadu poate fi găsită aici

  • Implementare

    O implementare nedocumentată prototip a Xanadu poate fi găsită aici – here. Rămîneţi cu noi!