Abstraktní datové typy a softwarová krize

Poznámka: Jedná se o část seriálu „Skládání softwaru“ (nyní kniha!) o výuce funkcionálního programování a kompozičních softwarových technik v jazyce JavaScriptES6+ od základů. Zůstaňte s námi. Čeká vás toho ještě hodně!
Koupit knihu | Rejstřík | < Předchozí | Další >

Nezaměňovat s:

Algebraické datové typy (někdy zkráceně ADT nebo AlgDT). Algebraické datové typy označují komplexní typy v programovacích jazycích (např. Rust, Haskell, F#), které zobrazují některé vlastnosti specifických algebraických struktur. např. součtové typy a součinové typy.

Algebraické struktury. Algebraické struktury se studují a aplikují z abstraktní algebry, která je stejně jako ADT také běžně specifikována pomocí algebraických popisů axiomů, ale použitelných daleko mimo svět počítačů a kódu. Může existovat algebraická struktura, kterou nelze softwarově zcela modelovat. Abstraktní datové typy naopak slouží jako specifikace a návod k formálnímu ověření fungujícího softwaru.

Abstraktní datový typ (ADT) je abstraktní koncept definovaný axiomy, které reprezentují nějaká data a operace s těmito daty. ADT nejsou definovány ve smyslu konkrétních instancí a nespecifikují konkrétní datové typy, struktury nebo algoritmy používané v implementacích. Místo toho ADT definují datové typy pouze z hlediska jejich operací a axiomů, které tyto operace musí dodržovat.

Obvyklé příklady ADT

  • Seznam
  • Stack
  • Queue
  • Set
  • Map
  • Stream

ADT mohou reprezentovat libovolnou množinu operací na libovolném druhu dat. Jinými slovy, vyčerpávající seznam všech možných ADT je nekonečný ze stejného důvodu, jako je nekonečný vyčerpávající seznam všech možných anglických vět. ADT jsou abstraktním pojmem množiny operací nad nespecifikovanými daty, nikoli konkrétní množinou konkrétních datových typů. Častým omylem je, že konkrétní příklady ADT, které se vyučují v mnoha univerzitních kurzech a učebnicích datových struktur, jsou tím, čím ADT jsou. Mnohé takové texty označují datové struktury jako „ADT“ a pak ADT vynechávají a místo toho popisují datové struktury konkrétními termíny, aniž by studenta kdy seznámily se skutečnou abstraktní reprezentací datového typu.

ADT mohou vyjadřovat mnoho užitečných algebraických struktur, včetně pologrup, monoidů, funktorů, monád atd. Specifikace Fantasyland je užitečný katalog algebraických struktur popsaných pomocí ADT, který podporuje interoperabilní implementace v jazyce JavaScript. Tvůrci knihoven mohou své implementace ověřovat pomocí dodaných axiomů.

Proč ADT?

Abstraktní datové typy jsou užitečné, protože nám poskytují způsob, jak formálně definovat opakovaně použitelné moduly způsobem, který je matematicky správný, přesný a jednoznačný. To nám umožňuje sdílet společný jazyk pro odkazování na rozsáhlý slovník užitečných softwarových stavebních bloků:

Historie ADT

V šedesátých a počátkem sedmdesátých let minulého století se mnoho programátorů a výzkumníků v oblasti informatiky zajímalo o krizi softwaru. Jak uvedl Edsger Dijkstra ve své přednášce o Turingově ceně:

„Hlavní příčinou softwarové krize je, že stroje se staly o několik řádů výkonnějšími! Zcela bez obalu řečeno: dokud nebyly stroje, programování nepředstavovalo žádný problém; když jsme měli několik slabých počítačů, programování se stalo mírným problémem a nyní máme gigantické počítače, programování se stalo stejně gigantickým problémem.“

Problém, o kterém mluví, spočívá v tom, že software je velmi složitý. Tištěná verze lunárního modulu Apollo a naváděcího systému pro NASA je vysoká asi jako skříň na dokumenty. To je spousta kódu. Představte si, že se snažíte přečíst a pochopit každý jeho řádek.

Moderní software je řádově složitější. Facebook měl v roce 2015 zhruba 62 milionů řádků kódu. Kdybyste vytiskli 50 řádků na stránku, zaplnili byste 1,24 milionu stránek. Kdybyste tyto stránky poskládali na sebe, získali byste zhruba 1 800 stránek na stopu, tedy 688 stop. To je více než sanfranciská věž Millenium Tower, která je v době psaní tohoto článku nejvyšší obytnou budovou v San Franciscu.

Zvládnutí složitosti softwaru je jedním z hlavních problémů, kterým čelí prakticky každý vývojář softwaru. V 60. a 70. letech minulého století neměli k dispozici jazyky, vzory ani nástroje, které dnes považujeme za samozřejmost. Věci jako lintery, intellisense a dokonce ani nástroje statické analýzy ještě nebyly vynalezeny.

Mnozí softwaroví inženýři si všimli, že hardware, na kterém věci stavěli, většinou fungoval. Ale software byl častěji složitý, zamotaný a křehký. Software byl běžně:

  • Překročený rozpočet
  • Zpožděný
  • Bugovitý
  • Chybějící požadavky
  • Složitý na údržbu

Kdybyste o softwaru dokázali uvažovat v modulárních částech, nemuseli byste rozumět celému systému, abyste pochopili, jak část systému zprovoznit. Tento princip návrhu softwaru se nazývá lokálnost. Abyste dosáhli lokality, potřebujete moduly, které můžete pochopit izolovaně od zbytku systému. Měli byste být schopni modul jednoznačně popsat, aniž byste příliš specifikovali jeho implementaci. To je problém, který řeší ADT.

Od 60. let 20. století až téměř do současnosti byl pokrok ve stavu modularity softwaru hlavním zájmem. Právě s ohledem na tyto problémy pracovali lidé včetně Barbary Liskovové (téže Liskovové, na kterou odkazuje Liskovův princip substituce ze zásad návrhu OO SOLID), Alana Kaye, Bertranda Meyera a dalších legend informatiky na popisu a specifikaci různých nástrojů umožňujících modulární software, včetně ADT, objektově orientovaného programování, respektive návrhu podle smlouvy.

ADT vznikly na základě práce Liskovové a jejích studentů na programovacím jazyku CLU v letech 1974 až 1975. Významně přispěli k současnému stavu vývoje specifikace softwarových modulů – jazyka, který používáme k popisu rozhraní umožňujících interakci softwarových modulů. Formálně dokazatelná shoda rozhraní nás výrazně přibližuje k modularitě a interoperabilitě softwaru.

Liskovová získala v roce 2008 Turingovu cenu za svou práci v oblasti abstrakce dat, odolnosti proti chybám a distribuovaných počítačů. ADT hrály v tomto úspěchu významnou roli a dnes prakticky každý univerzitní kurz informatiky zahrnuje ADT do učebních osnov.

Softwarová krize nebyla nikdy zcela vyřešena a mnohé z výše popsaných problémů by měl znát každý profesionální vývojář, ale naučit se používat nástroje, jako jsou objekty, moduly a ADT, jistě pomůže.

Specifikace ADT

K posouzení vhodnosti specifikace ADT lze použít několik kritérií. Já tato kritéria nazývám FAMED, ale tuto mnemotechnickou pomůcku jsem pouze vymyslel. Původní kritéria publikovali Liskov a Zilles ve svém slavném článku „Specification Techniques for Data Abstractions“ z roku 1975.

  • Formální. Specifikace musí být formální. Význam každého prvku ve specifikaci musí být definován dostatečně podrobně, aby cílová skupina měla poměrně dobrou šanci sestavit ze specifikace vyhovující implementaci. Musí být možné implementovat algebraický důkaz v kódu pro každý axiom ve specifikaci.
  • Použitelné. ADT by měly být široce použitelné. ADT by mělo být obecně opakovaně použitelné pro mnoho různých konkrétních případů použití. ADT, který popisuje konkrétní implementaci v konkrétním jazyce v konkrétní části kódu, pravděpodobně věci příliš specifikuje. Místo toho se ADT nejlépe hodí k popisu chování běžných datových struktur, knihovních komponent, modulů, vlastností programovacího jazyka atd. Například ADT popisující operace se zásobníkem nebo ADT popisující chování slibu.
  • Minimální. Specifikace ADT by měly být minimální. Specifikace by měla obsahovat zajímavé a široce použitelné části chování a nic víc. Každé chování by mělo být popsáno přesně a jednoznačně, ale s co nejmenším množstvím specifických nebo konkrétních detailů. Většina specifikací ADT by měla být dokazatelná pomocí několika axiomů.
  • Rozšiřitelnost. ADT by měly být rozšiřitelné. Malá změna požadavku by měla vést jen k malé změně specifikace.
  • Deklarativní. Deklarativní specifikace popisují co, nikoliv jak. ADT by měly být popsány z hlediska toho, co jsou věci, a mapování vztahů mezi vstupy a výstupy, nikoliv kroky k vytvoření datových struktur nebo konkrétní kroky, které musí každá operace provést.

Dobrá ADT by měla obsahovat:

  • Lidsky čitelný popis. ADT mohou být poněkud strohé, pokud nejsou doplněny nějakým lidsky čitelným popisem. Popis v přirozeném jazyce v kombinaci s algebraickými definicemi může fungovat jako vzájemná kontrola, která vyjasní případné chyby ve specifikaci nebo nejasnosti v jejím chápání čtenářem.
  • Definice. Jasně definujte všechny pojmy použité ve specifikaci, abyste předešli jakýmkoli nejasnostem.
  • Abstraktní signatury. Popište očekávané vstupy a výstupy, aniž byste je spojovali s konkrétními typy nebo datovými strukturami.
  • Axiomy. 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.
  • Abstraktní datové typy se zaměřují na to, co, nikoliv jak (jsou formulovány deklarativně a nespecifikují algoritmy nebo datové struktury).
  • Mezi běžné příklady patří seznamy, zásobníky, množiny atd.
  • ADT nám poskytují způsob, jak formálně definovat opakovaně použitelné moduly způsobem, který je matematicky správný, přesný a jednoznačný.
  • ADT vznikly na základě práce Liskova a jeho studentů na programovacím jazyku CLU v 70. letech.
  • ADT by měly být FAMED. Formální, široce použitelné, minimální, rozšiřitelné a deklarativní.
  • ADT by měly obsahovat lidsky čitelný popis, definice, abstraktní signatury a formálně ověřitelné axiomy.

Bonusový tip: Pokud si nejste jisti, zda byste měli funkci zapouzdřit, zeptejte se sami sebe, zda byste ji zahrnuli do ADT pro vaši komponentu. Pamatujte, že ADT by měly být minimální, takže pokud není nezbytná, postrádá soudržnost s ostatními operacemi nebo se její specifikace pravděpodobně změní, zapouzdřete ji.

Glosář

  • Axiomy jsou matematicky podložená tvrzení, která musí platit.
  • Matematicky solidní znamená, že každý pojem je dobře matematicky definován, takže je možné na jejich základě napsat jednoznačná a dokazatelná tvrzení o skutečnosti.

Další kroky

EricElliottJS.com obsahuje mnoho hodin video lekcí a interaktivních cvičení na podobná témata. Pokud se vám tento obsah líbí, zvažte, zda se k němu nepřidáte.

Napsat komentář

Vaše e-mailová adresa nebude zveřejněna. Vyžadované informace jsou označeny *