Abstrakta datatyper och programvarukrisen

Note: Det här är en del av serien ”Composing Software” (nu en bok!) om hur man lär sig funktionell programmering och kompositionella programvarutekniker i JavaScriptES6+ från grunden. Håll dig uppdaterad. Det kommer att komma mycket mer av detta!
Köp boken | Index | < Föregående | Nästa >

Försök inte förväxlas med:

Algebraiska datatyper (ibland förkortade ADT eller AlgDT). Algebraiska datatyper avser komplexa typer i programmeringsspråk (t.ex. Rust, Haskell, F#) som visar vissa egenskaper hos specifika algebraiska strukturer, t.ex. summetyper och produkttyper.

Algebraiska strukturer. Algebraiska strukturer studeras och tillämpas från abstrakt algebra, som liksom ADT:er också vanligtvis specificeras i termer av algebraiska beskrivningar av axiom, men som är tillämpliga långt utanför datorernas och kodens värld. Det kan finnas en algebraisk struktur som är omöjlig att modellera fullständigt i programvara. Däremot fungerar abstrakta datatyper som en specifikation och vägledning för att formellt verifiera fungerande programvara.

En abstrakt datatyp (ADT) är ett abstrakt begrepp som definieras av axiom som representerar vissa data och operationer på dessa data. ADT:er definieras inte i form av konkreta instanser och specificerar inte de konkreta datatyper, strukturer eller algoritmer som används i implementationer. Istället definierar ADT:er datatyper endast i termer av deras operationer och de axiom som dessa operationer måste följa.

Högre ADT-exempel

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

ADT:er kan representera vilken uppsättning av operationer som helst på vilken typ av data som helst. Med andra ord är den uttömmande listan över alla möjliga ADT:er oändlig av samma skäl som den uttömmande listan över alla möjliga engelska meningar är oändlig. ADT:er är det abstrakta konceptet för en uppsättning operationer över ospecificerade data, inte en specifik uppsättning konkreta datatyper. En vanlig missuppfattning är att de specifika exempel på ADT som lärs ut i många universitetskurser och läroböcker om datastruktur är vad ADT är. Många sådana texter märker datastrukturerna med ”ADT” och hoppar sedan över ADT och beskriver datastrukturerna i konkreta termer i stället, utan att någonsin utsätta studenten för en faktisk abstrakt representation av datatypen. Oops!

ADTs kan uttrycka många användbara algebraiska strukturer, inklusive semigrupper, monoider, funktorer, monader osv. Fantasyland Specification är en användbar katalog över algebraiska strukturer som beskrivs av ADT:er för att uppmuntra interoperabla implementeringar i JavaScript. Biblioteksbyggare kan verifiera sina implementationer med hjälp av de medföljande axiomen.

Varför ADT:s?

Abstrakta datatyper är användbara eftersom de ger oss ett sätt att formellt definiera återanvändbara moduler på ett sätt som är matematiskt sunt, exakt och entydigt. Detta gör det möjligt för oss att använda ett gemensamt språk för att hänvisa till en omfattande vokabulär av användbara programvarubyggblock: Idéer som är användbara att lära sig och bära med sig när vi rör oss mellan olika domäner, ramverk och till och med programmeringsspråk.

Historia om ADT:er

På 1960-talet och i början av 1970-talet var många programmerare och forskare inom datavetenskap intresserade av programvarukrisen. Som Edsger Dijkstra uttryckte det i sin Turingprisföreläsning:

”Den viktigaste orsaken till programvarukrisen är att maskinerna har blivit flera storleksordningar kraftfullare! För att säga det rent ut: så länge det inte fanns några maskiner var programmering inget problem alls; när vi hade några svaga datorer blev programmering ett lindrigt problem, och nu när vi har gigantiska datorer har programmering blivit ett lika gigantiskt problem.”

Problemet som han hänvisar till är att mjukvara är mycket komplicerad. En tryckt version av Apollo månmodul och styrsystem för NASA är ungefär lika hög som ett arkivskåp. Det är mycket kod. Tänk dig att försöka läsa och förstå varje rad i den.

Moderna programvaror är storleksordningar mer komplicerade. Facebook bestod 2015 av ungefär 62 miljoner rader kod. Om du skrev ut 50 rader per sida skulle du fylla 1,24 miljoner sidor. Om du staplar dessa sidor får du ungefär 1 800 sidor per fot, eller 688 fot. Det är högre än San Franciscos Millenium Tower, det högsta bostadshuset i San Francisco när detta skrivs.

Hantering av mjukvarukomplexitet är en av de främsta utmaningarna som praktiskt taget alla mjukvaruutvecklare står inför. På 1960- och 1970-talen hade de inte de språk, mönster eller verktyg som vi tar för givet idag. Saker som linters, intellisense och till och med statiska analysverktyg hade ännu inte uppfunnits.

Många programvaruingenjörer noterade att den hårdvara som de byggde saker ovanpå för det mesta fungerade. Men programvaran var oftast komplex, trasslig och bräcklig. Programvara var ofta:

• Over budget
• Sena
• Buggy
• Missade krav
• Svårt att underhålla

Om man bara kunde tänka på mjukvara i modulära bitar, skulle man inte behöva förstå hela systemet för att förstå hur man får en del av systemet att fungera. Denna princip för programvarudesign är känd som lokalitet. För att få lokalitet behöver du moduler som du kan förstå isolerat från resten av systemet. Du bör kunna beskriva en modul otvetydigt utan att överspecificera dess implementering. Det är det problemet som ADT:erna löser.

Från 1960-talet och nästan ända fram till i dag har det varit en central angelägenhet att förbättra moduleringen av programvara. Det var med dessa problem i åtanke som personer som Barbara Liskov (samma Liskov som det hänvisas till i Liskov Substitution Principle från SOLID OO-designprinciperna), Alan Kay, Bertrand Meyer och andra legender inom datavetenskapen arbetade med att beskriva och specificera olika verktyg för att möjliggöra modulär mjukvara, inklusive ADT:er, objektorienterad programmering respektive design by contract.

ADT:erna uppstod genom Liskovs och hennes studenters arbete med programmeringsspråket CLU mellan 1974 och 1975. De bidrog i hög grad till den senaste tekniken för specifikation av programvarumoduler – det språk vi använder för att beskriva de gränssnitt som gör det möjligt för programvarumoduler att interagera. Formellt bevisbar gränssnittsöverensstämmelse för oss betydligt närmare modularitet och driftskompatibilitet för programvara.

Liskov tilldelades Turingpriset för sitt arbete med dataabstraktion, feltolerans och distribuerad databehandling 2008. ADT:er spelade en viktig roll i den prestationen, och i dag ingår ADT:er i läroplanen i praktiskt taget varje universitetskurs i datavetenskap.

Mjukvarukrisen löstes aldrig helt, och många av de problem som beskrivs ovan bör vara bekanta för alla professionella utvecklare, men att lära sig använda verktyg som objekt, moduler och ADT:er är definitivt till hjälp.

Specifikationer för ADT:er

Flera kriterier kan användas för att bedöma lämpligheten hos en ADT-specifikation. Jag kallar dessa kriterier för FAMED, men jag har bara uppfunnit den mnemoniska metoden. De ursprungliga kriterierna publicerades av Liskov och Zilles i deras berömda artikel från 1975, ”Specification Techniques for Data Abstractions.”

• Formellt. Specifikationer måste vara formella. Betydelsen av varje element i specifikationen måste definieras tillräckligt detaljerat för att målgruppen ska ha en rimligt god chans att konstruera ett kompatibelt genomförande utifrån specifikationen. Det måste vara möjligt att implementera ett algebraiskt bevis i kod för varje axiom i specifikationen.
• Tillämpligt. ADT:er bör vara allmänt tillämpbara. En ADT bör i allmänhet kunna återanvändas för många olika konkreta användningsfall. En ADT som beskriver ett särskilt genomförande i ett särskilt språk i en särskild del av koden överspecificerar förmodligen saker och ting. ADT:er lämpar sig i stället bäst för att beskriva beteendet hos vanliga datastrukturer, bibliotekskomponenter, moduler, programmeringsspråksfunktioner osv. Till exempel en ADT som beskriver stackoperationer eller en ADT som beskriver beteendet hos ett löfte.
• Minimal. ADT-specifikationerna bör vara minimala. Specifikationen bör innehålla de intressanta och allmänt tillämpliga delarna av beteendet och inget mer. Varje beteende bör beskrivas exakt och otvetydigt, men med så få specifika eller konkreta detaljer som möjligt. De flesta ADT-specifikationer bör kunna bevisas med hjälp av en handfull axiom.
• Utökningsbar. ADT:er bör kunna utvidgas. En liten ändring i ett krav bör leda till endast en liten ändring i specifikationen.
• Deklarativ. Deklarativa specifikationer beskriver vad, inte hur. ADT:er bör beskrivas i termer av vad saker och ting är, och relationella mappningar mellan in- och utgångar, inte stegen för att skapa datastrukturer eller de specifika steg som varje operation måste utföra.

En bra ADT bör innehålla:

• Människoläsbar beskrivning. ADT:er kan vara ganska kortfattade om de inte åtföljs av en människoläsbar beskrivning. Den naturliga språkliga beskrivningen kan i kombination med de algebraiska definitionerna fungera som kontroller av varandra för att reda ut eventuella misstag i specifikationen eller tvetydigheter i läsarens förståelse av den.
• Definitioner. Definiera tydligt alla termer som används i specifikationen för att undvika tvetydigheter.
• Abstrakta signaturer. Beskriv de förväntade in- och utgångarna utan att koppla dem till konkreta typer eller datastrukturer.
• Axiom. 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.
• Abstrakta datatyper fokuserar på vad, inte hur (de är utformade deklarativt och specificerar inte algoritmer eller datastrukturer).
• Vanliga exempel är listor, staplar, uppsättningar osv.
• ADTs ger oss ett sätt att formellt definiera återanvändbara moduler på ett sätt som är matematiskt sunt, exakt och otvetydigt.
• ADTs uppstod ur Liskovs och studenters arbete med programmeringsspråket CLU på 1970-talet.
• ADTs bör vara FAMED. Formell, allmänt tillämplig, minimal, utvidgbar och deklarativ.
• ADT:er bör innehålla en människoläsbar beskrivning, definitioner, abstrakta signaturer och formellt verifierbara axiom.

Bonustips: Om du är osäker på om du ska kapsla in en funktion eller inte, fråga dig själv om du skulle inkludera den i en ADT för din komponent. Kom ihåg att ADT:er ska vara minimala, så om den är oviktig, saknar sammanhållning med de andra operationerna eller om dess specifikation sannolikt kommer att ändras, inkapsla den.

Glossar

• Axiom är matematiskt sunda påståenden som måste vara sanna.
• Matematiskt sunda innebär att varje term är väldefinierad matematiskt så att det är möjligt att skriva otvetydiga och bevisbara faktautsagor baserade på dem.

Nästa steg

EricElliottJS.com innehåller många timmars videolektioner och interaktiva övningar om ämnen som detta. Om du gillar det här innehållet kan du överväga att ansluta dig.