Abstracte gegevenstypen en de softwarecrisis

Note: dit maakt deel uit van de serie “Composing Software” (nu een boek!) over het van de grond af aan leren van functioneel programmeren en compositionele softwaretechnieken in JavaScriptES6+. Blijf op de hoogte. Er komt nog veel meer van dit!
Koop het boek | Index | < Vorige | Volgende >

Niet te verwarren met:

Algebraïsche Data Types (soms afgekort tot ADT of AlgDT). Algebraic Data Types verwijzen naar complexe typen in programmeertalen (bijv. Rust, Haskell, F#) die enkele eigenschappen van specifieke algebraïsche structuren vertonen. bijv. somtypen en producttypen.

Algebraïsche Structuren. Algebraïsche structuren worden bestudeerd en toegepast vanuit abstracte algebra’s, die net als ADT’s ook gewoonlijk worden gespecificeerd in termen van algebraïsche beschrijvingen van axioma’s, maar die ver buiten de wereld van computers en code toepasbaar zijn. Er kan een algebraïsche structuur bestaan die onmogelijk volledig in software kan worden gemodelleerd. Abstracte Gegevenstypen daarentegen dienen als specificatie en leidraad om werkende software formeel te verifiëren.

Een Abstract Gegevenstype (ADT) is een abstract concept gedefinieerd door axioma’s die bepaalde gegevens en bewerkingen op die gegevens representeren. ADT’s worden niet gedefinieerd in termen van concrete instanties en specificeren niet de concrete datatypen, structuren of algoritmen die in implementaties worden gebruikt. In plaats daarvan definiëren ADT’s gegevenstypen alleen in termen van hun bewerkingen, en de axioma’s waaraan die bewerkingen moeten voldoen.

Gemeenschappelijke ADT Voorbeelden

• Lijst
• Stack
• Queue
• Set
• Map
• Stream

ADT’s kunnen elke verzameling bewerkingen op elk soort gegevens representeren. Met andere woorden, de uitputtende lijst van alle mogelijke ADTs is oneindig om dezelfde reden dat de uitputtende lijst van alle mogelijke Engelse zinnen oneindig is. ADT’s zijn het abstracte concept van een reeks operaties over niet gespecificeerde gegevens, niet een specifieke reeks van concrete gegevenstypen. Een veel voorkomende misvatting is dat de specifieke voorbeelden van ADT’s die in veel universitaire cursussen en leerboeken over gegevensstructuren worden onderwezen, zijn wat ADT’s zijn. Veel van dergelijke teksten labelen de gegevensstructuren als “ADT’s” en slaan dan de ADT over en beschrijven de gegevensstructuren in plaats daarvan in concrete termen, zonder de student ooit bloot te stellen aan een werkelijke abstracte voorstelling van het gegevenstype. Oeps!

ADT’s kunnen veel nuttige algebraïsche structuren uitdrukken, waaronder semigroepen, monoïden, functoren, monads, enz. De Fantasyland Specification is een nuttige catalogus van algebraïsche structuren die door ADT’s worden beschreven om interoperabele implementaties in JavaScript te bevorderen. Bibliotheekbouwers kunnen hun implementaties verifiëren met behulp van de meegeleverde axioma’s.

Waarom ADT’s?

Abstracte Data Types zijn nuttig omdat ze ons een manier bieden om herbruikbare modules formeel te definiëren op een manier die wiskundig verantwoord, precies en ondubbelzinnig is. Dit laat ons toe een gemeenschappelijke taal te gebruiken om te verwijzen naar een uitgebreide woordenschat van nuttige software bouwstenen: Ideeën die nuttig zijn om te leren en met ons mee te dragen als we ons tussen domeinen, raamwerken en zelfs programmeertalen bewegen.

Geschiedenis van ADT’s

In de jaren zestig en begin jaren zeventig waren veel programmeurs en onderzoekers in de informatica geïnteresseerd in de softwarecrisis. Zoals Edsger Dijkstra het verwoordde in zijn Turing-prijslezing:

“De belangrijkste oorzaak van de softwarecrisis is dat de machines enkele ordes van grootte krachtiger zijn geworden! Om het maar eens ronduit te zeggen: zolang er geen machines waren, was programmeren geen enkel probleem; toen we een paar zwakke computers hadden, werd programmeren een mild probleem, en nu we gigantische computers hebben, is programmeren een al even gigantisch probleem geworden.”

Het probleem waar hij op doelt, is dat software erg ingewikkeld is. Een geprinte versie van de Apollo maanmodule en het geleidingssysteem voor NASA is ongeveer zo hoog als een archiefkast. Dat is een heleboel code. Stel je voor dat je elke regel daarvan probeert te lezen en te begrijpen.

Moderne software is ordes van grootte gecompliceerder. Facebook telde in 2015 ruwweg 62 miljoen regels code. Als je 50 regels per pagina zou afdrukken, zou je 1,24 miljoen pagina’s vullen. Als je die pagina’s stapelt, krijg je ongeveer 1.800 pagina’s per voet, of 688 voet. Dat is hoger dan de Millenium Tower in San Francisco, het hoogste woongebouw in San Francisco op het moment van schrijven.

Het beheren van de complexiteit van software is een van de belangrijkste uitdagingen waar vrijwel elke software-ontwikkelaar mee te maken krijgt. In de jaren zestig en zeventig beschikten ze nog niet over de talen, patronen en gereedschappen die we vandaag de dag zo vanzelfsprekend vinden. Dingen als linters, intellisense en zelfs statische analyse tools waren nog niet uitgevonden.

Vele software-ingenieurs merkten op dat de hardware waar ze dingen op bouwden meestal wel werkte. Maar software was meestal complex, warrig en broos. Software was vaak:

• Boven budget
• Te laat
• Buggy
• Missende requirements
• Moeilijk te onderhouden

Als je maar in modulaire stukken over software kon denken, zou je niet het hele systeem hoeven te begrijpen om te begrijpen hoe je een deel van het systeem kunt laten werken. Dat principe van software-ontwerp staat bekend als lokalisatie. Om plaatsgebondenheid te krijgen, heb je modules nodig die je los van de rest van het systeem kunt begrijpen. Je moet in staat zijn om een module ondubbelzinnig te beschrijven zonder de implementatie ervan te veel te specificeren. Dat is het probleem dat ADT’s oplossen.

Van de jaren zestig tot bijna op de dag van vandaag was het verbeteren van de modulariteit van software een kernpunt van zorg. Het was met die problemen in het achterhoofd dat mensen als Barbara Liskov (dezelfde Liskov waarnaar wordt verwezen in het Liskov Substitution Principle uit de SOLID OO ontwerp principes), Alan Kay, Bertrand Meyer en andere legendes van de computerwetenschap werkten aan het beschrijven en specificeren van verschillende gereedschappen om modulaire software mogelijk te maken, waaronder ADTs, object-georiënteerd programmeren, en ontwerp door contract, respectievelijk.

ADTs kwamen voort uit het werk van Liskov en haar studenten aan de CLU programmeertaal tussen 1974 en 1975. Zij hebben een belangrijke bijdrage geleverd aan de ontwikkeling van de specificatie van softwaremodules – de taal die wij gebruiken om de interfaces te beschrijven die de interactie tussen softwaremodules mogelijk maken. Formeel bewijsbare interface compliance brengt ons aanzienlijk dichter bij software modulariteit en interoperabiliteit.

Liskov kreeg in 2008 de Turing award voor haar werk aan data abstraction, fault tolerance, and distributed computing. ADT’s speelden daarbij een belangrijke rol, en tegenwoordig zijn ADT’s in vrijwel elke universitaire informatica-opleiding opgenomen.

De softwarecrisis is nooit helemaal opgelost, en veel van de hierboven beschreven problemen zouden voor elke professionele ontwikkelaar bekend moeten zijn, maar het leren gebruiken van gereedschappen als objecten, modules en ADT’s helpt zeker.

Specificaties voor ADT’s

Er zijn verschillende criteria die kunnen worden gebruikt om de geschiktheid van een ADT-specificatie te beoordelen. Ik noem deze criteria FAMED, maar ik heb het ezelsbruggetje alleen maar uitgevonden. De oorspronkelijke criteria zijn gepubliceerd door Liskov en Zilles in hun beroemde paper uit 1975, “Specification Techniques for Data Abstractions.”

• Formeel. Specificaties moeten formeel zijn. De betekenis van elk element in de specificatie moet voldoende gedetailleerd worden omschreven, zodat het doelpubliek een redelijk goede kans heeft om een implementatie te construeren die aan de specificatie voldoet. Het moet mogelijk zijn om een algebraïsch bewijs in code te implementeren voor elk axioma in de specificatie.
• Toepasbaar. ADT’s moeten algemeen toepasbaar zijn. Een ADT moet in het algemeen herbruikbaar zijn voor veel verschillende concrete use-cases. Een ADT die een bepaalde implementatie in een bepaalde taal in een bepaald deel van de code beschrijft, is waarschijnlijk overgespecificeerd. In plaats daarvan zijn ADTs het best geschikt om het gedrag te beschrijven van gemeenschappelijke gegevensstructuren, bibliotheekcomponenten, modules, programmeertaalkenmerken, enz. Bijvoorbeeld, een ADT die stack operaties beschrijft, of een ADT die het gedrag van een belofte beschrijft.
• Minimaal. ADT-specificaties moeten minimaal zijn. De specificatie moet de interessante en algemeen toepasbare delen van het gedrag bevatten en niets meer. Elk gedrag moet precies en ondubbelzinnig worden beschreven, maar in zo weinig mogelijk specifieke of concrete details. De meeste ADT-specificaties zouden bewijsbaar moeten zijn met behulp van een handvol axioma’s.
• Uitbreidbaar. ADT’s moeten uitbreidbaar zijn. Een kleine verandering in een eis zou slechts tot een kleine verandering in de specificatie moeten leiden.
• Declaratief. Declaratieve specificaties beschrijven wat, niet hoe. ADT’s moeten worden beschreven in termen van wat dingen zijn, en relatie mappings tussen inputs en outputs, niet de stappen om datastructuren te maken of de specifieke stappen die elke operatie moet uitvoeren.

Een goede ADT moet bevatten:

• Menselijk leesbare beschrijving. ADT’s kunnen nogal beknopt zijn als ze niet vergezeld gaan van een door mensen leesbare beschrijving. De beschrijving in natuurlijke taal kan, in combinatie met de algebraïsche definities, als controle op elkaar fungeren om eventuele fouten in de specificatie of onduidelijkheden in het begrip ervan door de lezer op te helderen.
• Definities. Definieer duidelijk alle termen die in de specificatie worden gebruikt om onduidelijkheden te voorkomen.
• Abstracte handtekeningen. Beschrijf de verwachte inputs en outputs zonder ze te koppelen aan concrete types of datastructuren.
• Axioma’s. 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.
• Abstracte Gegevenstypen zijn gericht op wat, niet hoe (ze zijn declaratief geformuleerd, en specificeren geen algoritmen of gegevensstructuren).
• Bekende voorbeelden zijn lijsten, stapels, verzamelingen, enz.
• ADT’s bieden ons een manier om herbruikbare modules formeel te definiëren op een manier die wiskundig verantwoord, precies en ondubbelzinnig is.
• ADT’s zijn voortgekomen uit het werk van Liskov en studenten aan de CLU-programmeertaal in de jaren zeventig.
• ADT’s moeten FAMED zijn. Formeel, breed toepasbaar, minimaal, uitbreidbaar en declaratief.
• ADT’s moeten een menselijk leesbare beschrijving, definities, abstracte handtekeningen en formeel verifieerbare axioma’s bevatten.

Bonustip: Als je niet zeker weet of je een functie wel of niet moet inkapselen, vraag jezelf dan af of je deze zou opnemen in een ADT voor je component. Onthoud dat ADT’s minimaal moeten zijn, dus als de functie niet essentieel is, geen samenhang heeft met de andere operaties, of de specificatie ervan waarschijnlijk zal veranderen, kapselt u hem in.

Glossary

• Axioma’s zijn wiskundig verantwoorde uitspraken die waar moeten zijn.
• Met wiskundig verantwoord wordt bedoeld dat elke term wiskundig goed gedefinieerd is, zodat het mogelijk is om er ondubbelzinnige en bewijsbare uitspraken op te baseren.

Volgende stappen

EricElliottJS.com bevat vele uren videolessen en interactieve oefeningen over onderwerpen als deze. Als deze inhoud u bevalt, kunt u overwegen lid te worden.