Les types de données abstraits et la crise du logiciel

Note : Ceci fait partie de la série « Composing Software » (maintenant un livre !) sur l’apprentissage de la programmation fonctionnelle et des techniques de composition de logiciels en JavaScriptES6+ à partir de la base. Restez à l’écoute. Il y a beaucoup plus de ceci à venir !
Acheter le livre | Index | < Précédent | Suivant >

Ne pas confondre avec:

Les types de données algébriques (parfois abrégés en ADT ou AlgDT). Les types de données algébriques font référence à des types complexes dans les langages de programmation (par exemple, Rust, Haskell, F#) qui affichent certaines propriétés de structures algébriques spécifiques. par exemple, les types de somme et les types de produit.

Structures algébriques. Les structures algébriques sont étudiées et appliquées à partir de l’algèbre abstraite, qui, comme les ADT, sont aussi couramment spécifiées en termes de descriptions algébriques d’axiomes, mais applicables bien en dehors du monde des ordinateurs et du code. Il peut exister une structure algébrique qu’il est impossible de modéliser complètement en logiciel. En revanche, les types de données abstraits servent de spécification et de guide pour vérifier formellement les logiciels qui fonctionnent.

Un type de données abstrait (ADT) est un concept abstrait défini par des axiomes qui représentent certaines données et des opérations sur ces données. Les ADT ne sont pas définis en termes d’instances concrètes et ne spécifient pas les types de données, structures ou algorithmes concrets utilisés dans les implémentations. Au lieu de cela, les ADTs définissent les types de données uniquement en termes de leurs opérations, et des axiomes auxquels ces opérations doivent adhérer.

Exemples d’ADTs communs

• List
• Stack
• Queueue
• Set
• Map
• Stream

Les ADTs peuvent représenter n’importe quel ensemble d’opérations sur n’importe quel type de données. En d’autres termes, la liste exhaustive de toutes les ADT possibles est infinie pour la même raison que la liste exhaustive de toutes les phrases anglaises possibles est infinie. Les ADT sont le concept abstrait d’un ensemble d’opérations sur des données non spécifiées, et non un ensemble spécifique de types de données concrètes. Une idée fausse courante est que les exemples spécifiques de FOAD enseignés dans de nombreux cours universitaires et manuels de structure de données constituent ce que sont les FOAD. Beaucoup de ces textes étiquettent les structures de données « ADT », puis sautent l’ADT et décrivent les structures de données en termes concrets à la place, sans jamais exposer l’étudiant à une représentation abstraite réelle du type de données. Oups !

Les ADT peuvent exprimer de nombreuses structures algébriques utiles, notamment les semigroupes, les monoïdes, les foncteurs, les monades, etc. La spécification Fantasyland est un catalogue utile de structures algébriques décrites par les ADT pour encourager les implémentations interopérables en JavaScript. Les constructeurs de bibliothèques peuvent vérifier leurs implémentations à l’aide des axiomes fournis.

Pourquoi des ADT ?

Les types de données abstraits sont utiles car ils nous permettent de définir formellement des modules réutilisables d’une manière qui soit mathématiquement solide, précise et sans ambiguïté. Cela nous permet de partager un langage commun pour faire référence à un vocabulaire étendu de blocs de construction logiciels utiles : Des idées qu’il est utile d’apprendre et de transporter avec nous lorsque nous passons d’un domaine à l’autre, d’un framework à l’autre et même d’un langage de programmation à l’autre.

Histoire des ADT

Dans les années 1960 et au début des années 1970, de nombreux programmeurs et chercheurs en informatique se sont intéressés à la crise du logiciel. Comme l’a exprimé Edsger Dijkstra dans sa conférence du prix Turing :

« La cause majeure de la crise du logiciel est que les machines sont devenues plusieurs ordres de grandeur plus puissantes ! Pour le dire très crûment : tant qu’il n’y avait pas de machines, la programmation n’était pas du tout un problème ; lorsque nous avions quelques ordinateurs faibles, la programmation devenait un problème léger, et maintenant que nous avons des ordinateurs gigantesques, la programmation est devenue un problème tout aussi gigantesque. »

Le problème auquel il fait référence est que les logiciels sont très compliqués. Une version imprimée du module lunaire Apollo et du système de guidage de la NASA a la hauteur d’un classeur. Cela représente beaucoup de code. Imaginez que vous essayez de lire et de comprendre chaque ligne de celui-ci.

Les logiciels modernes sont des ordres de grandeur plus compliqués. Facebook représentait en gros 62 millions de lignes de code en 2015. Si vous imprimiez 50 lignes par page, vous rempliriez 1,24 million de pages. Si vous empilez ces pages, vous obtenez environ 1 800 pages par pied, soit 688 pieds. C’est plus haut que la Millenium Tower de San Francisco, le plus haut immeuble résidentiel de San Francisco au moment où nous écrivons ces lignes.

Gérer la complexité des logiciels est l’un des principaux défis auxquels sont confrontés pratiquement tous les développeurs de logiciels. Dans les années 1960 et 1970, ils ne disposaient pas des langages, des modèles ou des outils que nous tenons pour acquis aujourd’hui. Des choses comme les linters, l’intellisense et même les outils d’analyse statique n’étaient pas encore inventées.

De nombreux ingénieurs logiciels ont remarqué que le matériel sur lequel ils construisaient des choses fonctionnait la plupart du temps. Mais les logiciels, le plus souvent, étaient complexes, enchevêtrés et fragiles. Les logiciels étaient couramment :

• Dépassant le budget
• Tardifs
• Buggy
• Manque des exigences
• Difficile à maintenir

Si seulement vous pouviez penser aux logiciels en pièces modulaires, vous n’auriez pas besoin de comprendre l’ensemble du système pour comprendre comment faire fonctionner une partie du système. Ce principe de conception de logiciels est connu sous le nom de localité. Pour obtenir la localité, vous avez besoin de modules que vous pouvez comprendre indépendamment du reste du système. Vous devez être en mesure de décrire un module sans ambiguïté sans sur-spécifier son implémentation. C’est le problème que les ADTs résolvent.

Depuis les années 1960 presque jusqu’à aujourd’hui, faire progresser l’état de la modularité des logiciels était une préoccupation centrale. C’est avec ces problèmes à l’esprit que des personnes comme Barbara Liskov (la même Liskov référencée dans le principe de substitution de Liskov des principes de conception OO SOLID), Alan Kay, Bertrand Meyer et d’autres légendes de l’informatique ont travaillé à la description et à la spécification de divers outils permettant la modularité des logiciels, notamment les ADT, la programmation orientée objet et la conception par contrat, respectivement.

Les ADT sont nées des travaux de Liskov et de ses étudiants sur le langage de programmation CLU entre 1974 et 1975. Ils ont contribué de manière significative à l’état de l’art de la spécification des modules logiciels – le langage que nous utilisons pour décrire les interfaces qui permettent aux modules logiciels d’interagir. La conformité formellement prouvable des interfaces nous rapproche considérablement de la modularité et de l’interopérabilité des logiciels.

Liskov a reçu le prix Turing pour ses travaux sur l’abstraction de données, la tolérance aux pannes et l’informatique distribuée en 2008. Les ADT ont joué un rôle important dans cet accomplissement, et aujourd’hui, pratiquement tous les cours universitaires d’informatique incluent les ADT dans le programme.

La crise du logiciel n’a jamais été entièrement résolue, et beaucoup des problèmes décrits ci-dessus devraient être familiers à tout développeur professionnel, mais apprendre à utiliser des outils comme les objets, les modules et les ADT aide certainement.

Spécifications pour les ADT

Plusieurs critères peuvent être utilisés pour juger de la pertinence d’une spécification ADT. J’appelle ces critères FAMED, mais j’ai seulement inventé ce moyen mnémotechnique. Les critères originaux ont été publiés par Liskov et Zilles dans leur célèbre article de 1975, « Specification Techniques for Data Abstractions ».

• Formal. Les spécifications doivent être formelles. La signification de chaque élément de la spécification doit être définie de manière suffisamment détaillée pour que le public cible ait une chance raisonnable de construire une implémentation conforme à partir de la spécification. Il doit être possible d’implémenter une preuve algébrique dans le code pour chaque axiome de la spécification.
• Applicable. Les ADT doivent être largement applicables. Une ADT doit être généralement réutilisable pour de nombreux cas d’utilisation concrets différents. Un ADT qui décrit une implémentation particulière dans un langage particulier dans une partie particulière du code est probablement sur-spécifier les choses. Au lieu de cela, les ADT sont les mieux adaptés pour décrire le comportement des structures de données communes, des composants de bibliothèque, des modules, des caractéristiques du langage de programmation, etc. Par exemple, un ADT décrivant les opérations de pile, ou un ADT décrivant le comportement d’une promesse.
• Minimum. Les spécifications ADT doivent être minimales. La spécification doit inclure les parties intéressantes et largement applicables du comportement et rien de plus. Chaque comportement devrait être décrit avec précision et sans ambiguïté, mais avec le moins de détails spécifiques ou concrets possible. La plupart des spécifications ADT devraient être prouvables en utilisant une poignée d’axiomes.
• Extensible. Les ADTs devraient être extensibles. Un petit changement dans une exigence devrait conduire à seulement un petit changement dans la spécification.
• Déclarative. Les spécifications déclaratives décrivent quoi, pas comment. Les ADT doivent être décrites en termes de ce que sont les choses et de mappages de relations entre les entrées et les sorties, et non pas les étapes de création de structures de données ou les étapes spécifiques que chaque opération doit effectuer.

Un bon ADT doit inclure :

• Une description lisible par l’homme. Les ADT peuvent être plutôt laconiques si elles ne sont pas accompagnées d’une certaine description lisible par l’homme. La description en langage naturel, combinée aux définitions algébriques, peut agir comme des vérifications l’une sur l’autre pour éliminer toute erreur dans la spécification ou toute ambiguïté dans la compréhension du lecteur.
• Définitions. Définissez clairement tous les termes utilisés dans la spécification pour éviter toute ambiguïté.
• Signatures abstraites. Décrivez les entrées et les sorties attendues sans les relier à des types concrets ou à des structures de données.
• Axiomes. 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.
• Les types de données abstraits se concentrent sur le quoi, et non sur le comment (ils sont encadrés de manière déclarative, et ne spécifient pas d’algorithmes ou de structures de données).
• Les exemples courants incluent les listes, les piles, les ensembles, etc.
• Les ADT fournissent un moyen pour nous de définir formellement des modules réutilisables d’une manière qui est mathématiquement solide, précise et non ambiguë.
• Les ADT ont émergé du travail de Liskov et de ses étudiants sur le langage de programmation CLU dans les années 1970.
• Les ADT devraient être FAMED. Formel, largement applicable, minimal, extensible et déclaratif.
• Les ADT doivent inclure une description lisible par l’homme, des définitions, des signatures abstraites et des axiomes formellement vérifiables.

Conseil bonus : si vous n’êtes pas sûr de devoir encapsuler une fonction, demandez-vous si vous l’incluriez dans un ADT pour votre composant. N’oubliez pas que les ADT doivent être minimales, donc si elle n’est pas essentielle, qu’elle manque de cohésion avec les autres opérations ou que sa spécification est susceptible de changer, encapsulez-la.

Glossaire

• Les axiomes sont des énoncés mathématiquement solides qui doivent être vrais.
• Solides mathématiquement signifie que chaque terme est bien défini mathématiquement de sorte qu’il est possible d’écrire des déclarations de fait non ambiguës et prouvables basées sur eux.

Prochaines étapes

EricElliottJS.com propose plusieurs heures de leçons vidéo et d’exercices interactifs sur des sujets comme celui-ci. Si vous aimez ce contenu, envisagez de vous y joindre.

.