Informatique et Sciences du Numérique au lycée : un pas plus loin/LANGAGES
Introduction
[modifier | modifier le wikicode]L'enseignement de l'option ISN donne une première présentation des notions essentielles relatives à la programmation (notion de programme, boucles, types, fonctions, récursivité, etc.) et une initiation aux notions de langages formellement définis (par une grammaire) et de sémantiques. La présentation du domaine "Langages" propose une étude plus approfondie des notions liées à la programmation à travers les langages utilisés.
La partie Éléments de syntaxe et de sémantique décrit les notions essentielles des langages de programmation : langage défini par une grammaire, proposant différentes constructions syntaxiques permettant de représenter les données et de décrire les actions et calculs à effectuer par le programme. Sont donc présentées ici les notions de portée, affectation, boucles, fonctions et procédures. Vient ensuite la représentation des données à l'aide de types (types de base, types construits et filtrage, tableaux, chaînes de caractères, flots, pointeurs), d'objets et de classes. La structuration des programmes à l'aide du polymorphisme, des modules et foncteurs, des classes et objets, du chargement dynamique de code est ensuite traitée. Les notions de surcharge, coercion, sous-types, sérialisation-désérialisation sont également traitées. Cette partie présente ensuite différents styles de programmation : niveaux de langages, programmation séquentielle, synchronisme, concurrence, distribution. La page Langages de Programmation de Wikipedia présente succinctement certains points de cette partie.
Pour exprimer puis prouver des propriétés des objets que l'on manipule, on utilise en général un langage apparenté aux mathématiques et des règles qui permettent de bâtir un raisonnement. L'archétype de ces langages est la logique --- ou plus exactement les logiques --- mathématique. Toutes ces notions, nécessaires aux différents travaux de programmation, sont présentées dans la partie Éléments de Logique.
Les éléments de logique étant précisés, il est alors possible d'aborder la question : Comment exprimer ce que doit faire un programme? La spécification d'un programme exprime le résultat attendu de l'exécution d'un programme et elle est étudiée dans la partie Langages et outils de spécification. Elle est encore la plupart du temps exprimée en langage naturel et il en résulte souvent quelque ambigüité conduisant parfois à quelque désappointement. Bien entendu, certaines exigences sur le logiciel ne sont pas exprimables par une formule logique, quelle que soit la logique utilisée. Mais les ambigüités dans la spécification doivent être levées avant le début du développement du logiciel. Il faut toutefois se garder d'imposer des choix non nécessaires (autrement dit, éviter de sur-spécifier) afin de ne pas contraindre outre mesure l'expression de la spécification dans sa programmation. Par exemple, il est important de mentionner que la gestion des attentes de personnes à un service doit se faire sur le mode "premier entré-premier sorti" mais il n'est pas nécessaire de requérir dans la spécification que le groupe de personnes attendant soit représenté par une liste, un tableau, etc.
Pour traduire fidèlement une spécification dans le langage de programmation choisi, il est préférable de connaître très précisément la signification des constructions syntaxiques offertes par le langage, c'est-à-dire sa sémantique présentée dans la partie Sémantiques. La lecture seule du manuel de référence du langage utilisé est souvent insuffisante. Tout point resté obscur doit être exploré à l'aide d'exemples test judicieusement construits en s'appuyant sur des connaissances sémantiques préalablement acquises. Le chapitre Distorsions sémantiques présente quelques exemples de résultats d'exécution "inattendus", dus à des incohérences ou incompréhensions sémantiques. Elle justifie la présentation formelle des sémantiques adoptée dans cette partie. Par exemple, la signification du mot-cle private diffère d'un langage à l'autre et, dans un même langage, sa signification peut varier suivant sa place dans le programme source (à l'intérieur d'un module, dans une sous-classe, etc.).
La compilation est abordée dans la partie Compilation, qui décrit différentes possibilités de construction d'un exécutable à partir du texte en langage source, en se limitant toutefois aux langages dits séquentiels pour des questions de taille du wikilivre. Le chapitre Analyses lexicale et syntaxique présente les notions de langage formel et de grammaire avant d'introduire les analyses lexicale et syntaxique et la construction des Arbres de Syntaxe Abstraite (AST). Dans le chapitre Analyses sémantiques, sont décrits le typage et différentes analyses sémantiques effectuées dans la première phase de la compilation. La seconde phase est présentée dans le chapitre Génération de code qui regroupe les optimisations, la production de binaires, de bytecode et les opérations de chargement de code. Il contient également une présentation de l'interprétation.
Reste alors à s'assurer que l'exécution d'un programme répond à sa spécification. Des méthodes telles que le test, la relecture de code sont généralement utilisées. La partie Tests les présente. Les techniques de test ne peuvent révéler que les anomalies liées au choix du jeu de test examiné. Même si le taux de couverture d'un test est très élevé, il ne peut rien révéler sur les jeux de données non examinés et peut donc laisser des anomalies non détectées. Il n'en reste pas moins que les tests sont indispensables et ils sont d'ailleurs énormément utilisés dans la production industrielle de logiciels.
Si la robustesse d'un programme est essentielle, on peut se tourner vers les méthodes de vérification dites formelles pour augmenter la confiance dans le programme. Deux grandes familles de méthodes peuvent être utilisées. Soit on construit un modèle de l'exécution d'un programme permettant d'analyser la validité d'une certaine propriété recherchée sur une exécution. Soit, on traduit le code du programme (souvent le source mais parfois sa traduction dans du langage de plus bas niveau) dans un système d'aide à la preuve, dans lequel toutes les propriétés recherchées pourront être exprimées puis validées.
La première famille, présentée dans la partie Logiques Temporelles et Vérification par modèles utilise les logiques temporelles pour créer les modèles, analysés ensuite à l'aide de méthodes issues de la théorie des automates, qui constituent ce que l'on appelle la vérification par modèles.
La seconde famille, présentée dans la partie Théorie des Types et Assistants de Preuve, utilise soit la théorie des ensembles soit une logique dite d'ordre supérieur, encore nommée Théorie des Types. Il existe en fait plusieurs Théories des Types qui fondent différents outils d'aide à la preuve mathématique de correction de programmes.
