Tipurile de date abstracte și criza software-ului

Nota: Aceasta face parte din seria „Composing Software” (acum o carte!) despre învățarea de la zero a programării funcționale și a tehnicilor software compoziționale în JavaScriptES6+. Rămâneți la curent. Vor urma multe altele!
Cumpărați cartea | Index | < Precedent | Următor >

Nu trebuie confundat cu:

Tipuri de date algebrice (uneori abreviat ADT sau AlgDT). Tipurile de date algebrice se referă la tipuri complexe din limbajele de programare (de exemplu, Rust, Haskell, F#) care afișează unele proprietăți ale unor structuri algebrice specifice. de exemplu, tipuri de sumă și tipuri de produs.

Structuri algebrice. Structurile algebrice sunt studiate și aplicate din algebra abstractă, care, ca și ADT-urile, sunt, de asemenea, specificate în mod obișnuit în termeni de descrieri algebrice ale axiomelor, dar aplicabile cu mult în afara lumii calculatoarelor și a codurilor. Poate exista o structură algebrică care este imposibil de modelat complet în software. Prin contrast, tipurile de date abstracte servesc drept specificație și ghid pentru verificarea formală a software-ului funcțional.

Un tip de date abstracte (ADT) este un concept abstract definit prin axiome care reprezintă anumite date și operații asupra acestor date. ADT-urile nu sunt definite în termeni de instanțe concrete și nu specifică tipurile de date, structurile sau algoritmii concreți utilizați în implementări. În schimb, ADT-urile definesc tipurile de date numai în ceea ce privește operațiile lor și axiomele la care trebuie să adere aceste operații.

Exemple comune de ADT-uri

  • List
  • Stack
  • Queue
  • Set
  • Map
  • Stream

ADT-urile pot reprezenta orice set de operații asupra oricărui tip de date. Cu alte cuvinte, lista exhaustivă a tuturor ADT-urilor posibile este infinită din același motiv pentru care lista exhaustivă a tuturor propozițiilor posibile în limba engleză este infinită. ADT-urile reprezintă conceptul abstract al unui set de operații asupra unor date nespecificate, și nu un set specific de tipuri de date concrete. O concepție greșită frecventă este aceea că exemplele specifice de ADT predate în multe cursuri universitare și manuale de structură de date reprezintă ADT-urile. Multe astfel de texte etichetează structurile de date ca fiind „ADT-uri”, apoi sar peste ADT și descriu în schimb structurile de date în termeni concreți, fără a expune vreodată studentul la o reprezentare abstractă reală a tipului de date. Oops!

ADT-urile pot exprima multe structuri algebrice utile, inclusiv semigrupuri, monoizi, functori, monade, etc. Specificația Fantasyland este un catalog util de structuri algebrice descrise de ADT-uri pentru a încuraja implementările interoperabile în JavaScript. Constructorii de biblioteci își pot verifica implementările folosind axiomele furnizate.

De ce ADT-uri?

Tipurile abstracte de date sunt utile deoarece ne oferă o modalitate de a defini formal modulele reutilizabile într-un mod care este sănătos din punct de vedere matematic, precis și lipsit de ambiguitate. Acest lucru ne permite să împărtășim un limbaj comun pentru a ne referi la un vocabular extins de elemente de construcție software utile: Idei pe care este util să le învățăm și să le purtăm cu noi atunci când trecem de la un domeniu la altul, de la un cadru de lucru la altul și chiar de la un limbaj de programare la altul.

Istoria ADT-urilor

În anii 1960 și la începutul anilor 1970, mulți programatori și cercetători în domeniul informaticii au fost interesați de criza software. După cum a spus Edsger Dijkstra în prelegerea sa de decernare a premiului Turing:

„Cauza majoră a crizei software-ului este că mașinile au devenit cu câteva ordine de mărime mai puternice! Ca să spunem lucrurilor pe nume: atâta timp cât nu existau mașini, programarea nu era deloc o problemă; când am avut câteva calculatoare slabe, programarea a devenit o problemă ușoară, iar acum avem calculatoare gigantice, programarea a devenit o problemă la fel de gigantică.”

Problema la care se referă el este că software-ul este foarte complicat. O versiune tipărită a modulului lunar Apollo și a sistemului de ghidare pentru NASA are aproximativ înălțimea unui dulap de dosare. Este o mulțime de cod. Imaginați-vă că încercați să citiți și să înțelegeți fiecare linie din acesta.

Software-ul modern este cu câteva ordine de mărime mai complicat. Facebook avea aproximativ 62 de milioane de linii de cod în 2015. Dacă ați tipări 50 de linii pe pagină, ați umple 1,24 milioane de pagini. Dacă ați stivui acele pagini, ați obține aproximativ 1.800 de pagini pe picior, sau 688 de picioare. Acest lucru este mai înalt decât Millenium Tower din San Francisco, cea mai înaltă clădire rezidențială din San Francisco la momentul redactării acestui articol.

Managementul complexității software-ului este una dintre provocările principale cu care se confruntă practic fiecare dezvoltator de software. În anii 1960 și 1970, aceștia nu dispuneau de limbajele, modelele sau instrumentele pe care le considerăm de la sine înțelese astăzi. Lucruri precum linters, intellisense și chiar instrumentele de analiză statică nu fuseseră încă inventate.

Mulți ingineri de software au observat că hardware-ul pe care construiau lucruri funcționa în mare parte. Dar software-ul, de cele mai multe ori, era complex, încâlcit și fragil. Software-ul era în mod obișnuit:

  • Depășea bugetul
  • Târziu
  • Buggy
  • Lipsesc cerințele
  • Dificil de întreținut

Dacă ați putea să vă gândiți la software în bucăți modulare, nu ar fi nevoie să înțelegeți întregul sistem pentru a înțelege cum să faceți să funcționeze o parte din sistem. Acest principiu de proiectare a software-ului este cunoscut sub numele de localitate. Pentru a obține localitatea, aveți nevoie de module pe care le puteți înțelege în mod izolat de restul sistemului. Ar trebui să puteți descrie un modul fără ambiguitate fără a specifica în mod excesiv implementarea sa. Aceasta este problema pe care o rezolvă ADT-urile.

Începând cu anii 1960 aproape până în prezent, avansarea stadiului modularității software a fost o preocupare centrală. Ținând cont de aceste probleme, oameni precum Barbara Liskov (aceeași Liskov la care se face referire în Principiul de substituție Liskov din principiile de proiectare SOLID OO), Alan Kay, Bertrand Meyer și alte legende ale informaticii au lucrat la descrierea și specificarea diferitelor instrumente care să permită software modular, inclusiv ADT-urile, programarea orientată pe obiecte și, respectiv, proiectarea prin contract.

ADT-urile au apărut din munca lui Liskov și a studenților săi la limbajul de programare CLU între 1974 și 1975. Acestea au contribuit în mod semnificativ la stadiul actual al specificării modulelor software – limbajul pe care îl folosim pentru a descrie interfețele care permit modulelor software să interacționeze. Conformitatea formală demonstrabilă a interfețelor ne aduce semnificativ mai aproape de modularitatea și interoperabilitatea software.

Liskov a primit premiul Turing pentru activitatea sa privind abstractizarea datelor, toleranța la erori și calculul distribuit în 2008. ADT-urile au jucat un rol semnificativ în această realizare, iar astăzi, practic fiecare curs universitar de informatică include ADT-urile în programa școlară.

Criza software-ului nu a fost niciodată rezolvată în întregime, iar multe dintre problemele descrise mai sus ar trebui să fie familiare oricărui dezvoltator profesionist, dar învățarea modului de utilizare a unor instrumente precum obiectele, modulele și ADT-urile ajută cu siguranță.

Specificații pentru ADT-uri

Pe mai multe criterii pot fi folosite pentru a judeca adecvarea unei specificații ADT. Eu numesc aceste criterii FAMED, dar eu doar am inventat mnemotehnica. Criteriile originale au fost publicate de Liskov și Zilles în celebra lor lucrare din 1975, „Specification Techniques for Data Abstractions.”

  • Formal. Specificațiile trebuie să fie formale. Semnificația fiecărui element din specificație trebuie să fie definită suficient de detaliat pentru ca publicul țintă să aibă o șansă rezonabil de bună de a construi o implementare conformă din specificație. Trebuie să fie posibilă implementarea unei dovezi algebrice în cod pentru fiecare axiomă din specificație.
  • Aplicabil. ADT-urile trebuie să fie aplicabile pe scară largă. O ADT trebuie să fie în general reutilizabilă pentru multe cazuri de utilizare concrete diferite. Un ADT care descrie o anumită implementare într-un anumit limbaj, într-o anumită parte a codului, este probabil o supraspecificare a lucrurilor. În schimb, ADT-urile sunt cele mai potrivite pentru a descrie comportamentul structurilor de date comune, al componentelor de bibliotecă, al modulelor, al caracteristicilor limbajului de programare etc. De exemplu, un ADT care descrie operațiile stivei, sau un ADT care descrie comportamentul unei promisiuni.
  • Minimal. Specificațiile ADT ar trebui să fie minime. Specificația ar trebui să includă părțile interesante și aplicabile pe scară largă ale comportamentului și nimic mai mult. Fiecare comportament ar trebui să fie descris cu precizie și fără ambiguitate, dar cu cât mai puține detalii specifice sau concrete posibil. Majoritatea specificațiilor ADT ar trebui să poată fi dovedite folosind o mână de axiome.
  • Extensibil. ADT-urile ar trebui să fie extensibile. O mică schimbare într-o cerință ar trebui să ducă doar la o mică schimbare în specificație.
  • Declarativ. Specificațiile declarative descriu ce, nu cum. ADT-urile ar trebui să fie descrise în termeni de ceea ce sunt lucrurile și de corespondențe de relații între intrări și ieșiri, nu de pașii de creare a structurilor de date sau de etapele specifice pe care trebuie să le efectueze fiecare operațiune.

Un ADT bun ar trebui să includă:

  • Descriere lizibilă pentru oameni. ADT-urile pot fi destul de laconice dacă nu sunt însoțite de o descriere lizibilă de către om. Descrierea în limbaj natural, combinată cu definițiile algebrice, pot acționa ca verificări reciproce pentru a clarifica orice greșeli din specificație sau ambiguitate în înțelegerea acesteia de către cititor.
  • Definiții. Definiți în mod clar toți termenii utilizați în specificație pentru a evita orice ambiguitate.
  • Semnături abstracte. Descrieți intrările și ieșirile așteptate fără să le legați de tipuri concrete sau structuri de date.
  • Axiome. Algebraic definitions of the axiom invariants used to prove that an implementation has satisfied the requirements of the specification.

Stack ADT Example

A stack is a Last In, First Out (LIFO) pile of items which allows users to interact with the stack by pushing a new item to the top of the stack, or popping the most recently pushed item from the top of the stack.

Stacks are commonly used in parsing, sorting, and data collation algorithms.

Definitions

  • a: Any type
  • b: Any type
  • item: Any type
  • stack(): an empty stack
  • stack(a): a stack of a
  • : a pair of item and stack

Abstract Signatures

The stack operation takes any number of items and returns a stack of those items. Typically, the abstract signature for a constructor is defined in terms of itself. Please don’t confuse this with a recursive function.

  • stack(...items) => stack(...items)

Stack Operations (operations which return a stack)

  • push(item, stack()) => stack(item)
  • pop(stack) =>

Axioms

The stack axioms deal primarily with stack and item identity, the sequence of the stack items, and the behavior of pop when the stack is empty.

Identity

Pushing and popping have no side-effects. If you push to a stack and immediately pop from the same stack, the stack should be in the state it was before you pushed.

pop(push(a, stack())) = 
  • Given: push a to the stack and immediately pop from the stack
  • Should: return a pair of a and stack().

Sequence

Popping from the stack should respect the sequence: Last In, First Out (LIFO).

pop(push(b, push(a, stack())) = 
  • Given: push a to the stack, then push b to the stack, then pop from the stack
  • Should: return a pair of b and stack(a).

Empty

Popping from an empty stack results in an undefined item value. In concrete terms, this could be defined with a Maybe(item), Nothing, or Either. In JavaScript, it’s customary to use undefined. Popping from an empty stack should not change the stack.

pop(stack()) = 
  • Given: pop from an empty stack
  • Should: return a pair of undefined and stack().

Concrete Implementations

An abstract data type could have many concrete implementations, in different languages, libraries, frameworks, etc. Here is one implementation of the above stack ADT, using an encapsulated object, and pure functions over that object:

const stack = (...items) => ({
push: item => stack(...items, item),
pop: () => {
// create a item list
const newItems = ; // remove the last item from the list and
// assign it to a variable
const = newItems.splice(-1); // return the pair
return ;
},
// So we can compare stacks in our assert function
toString: () => `stack(${ items.join(',') })`
});const push = (item, stack) => stack.push(item);
const pop = stack => stack.pop();

And another that implements the stack operations in terms of pure functions over JavaScript’s existing Array type:

const stack = (...elements) => ;const push = (a, stack) => stack.concat();const pop = stack => {
const newStack = stack.slice(0);
const item = newStack.pop();
return ;
};

Both versions satisfy the following axiom proofs:

// A simple assert function which will display the results
// of the axiom tests, or throw a descriptive error if an
// implementation fails to satisfy an axiom.
const assert = ({given, should, actual, expected}) => {
const stringify = value => Array.isArray(value) ?
`` :
`${ value }`;
const actualString = stringify(actual);
const expectedString = stringify(expected);
if (actualString === expectedString) {
console.log(`OK:
given: ${ given }
should: ${ should }
actual: ${ actualString }
expected: ${ expectedString }
`);
} else {
throw new Error(`NOT OK:
given ${ given }
should ${ should }
actual: ${ actualString }
expected: ${ expectedString }
`);
}
};// Concrete values to pass to the functions:
const a = 'a';
const b = 'b';// Proofs
assert({
given: 'push `a` to the stack and immediately pop from the stack',
should: 'return a pair of `a` and `stack()`',
actual: pop(push(a, stack())),
expected:
})assert({
given: 'push `a` to the stack, then push `b` to the stack, then pop from the stack',
should: 'return a pair of `b` and `stack(a)`.',
actual: pop(push(b, push(a, stack()))),
expected:
});assert({
given: 'pop from an empty stack',
should: 'return a pair of undefined, stack()',
actual: pop(stack()),
expected:
});

Conclusion

  • An Abstract Data Type (ADT) is an abstract concept defined by axioms which represent some data and operations on that data.
  • Tipurile de date abstracte se concentrează pe ce, nu pe cum (sunt încadrate declarativ și nu specifică algoritmi sau structuri de date).
  • Exemple comune includ liste, stive, seturi, etc.
  • ADT-urile ne oferă o modalitate de a defini în mod formal module reutilizabile într-un mod care este matematic solid, precis și lipsit de ambiguitate.
  • ADT-urile au apărut din munca lui Liskov și a studenților la limbajul de programare CLU în anii 1970.
  • ADT-urile ar trebui să fie FAMED. Formal, aplicabil pe scară largă, minimal, extensibil și declarativ.
  • ADT-urile ar trebui să includă o descriere lizibilă pentru om, definiții, semnături abstracte și axiome verificabile formal.

Tip bonus: Dacă nu sunteți sigur dacă ar trebui sau nu să încapsulați o funcție, întrebați-vă dacă ați include-o într-o ADT pentru componenta dvs. Nu uitați, ADT-urile ar trebui să fie minime, așa că, dacă nu este esențială, nu are coeziune cu celelalte operații sau este posibil ca specificația sa să se schimbe, încapsulați-o.

Glosar

  • Axiomele sunt afirmații matematice solide care trebuie să fie adevărate.
  • Matematic solide înseamnă că fiecare termen este bine definit din punct de vedere matematic, astfel încât este posibil să se scrie afirmații de fapt neechivoce și demonstrabile pe baza lor.

Pași următori

EricElliottJS.com oferă multe ore de lecții video și exerciții interactive pe teme ca aceasta. Dacă vă place acest conținut, vă rugăm să luați în considerare posibilitatea de a vă înscrie.

.

Lasă un răspuns

Adresa ta de email nu va fi publicată. Câmpurile obligatorii sunt marcate cu *