===== Fondements de la programmation =====

Un objectif de ce cours est de découvrir sur quoi repose la programmation en se basant sur l'étude des programmes et des langages.

Les langages révèlent des modes de programmation. Mais qu'est-ce qu'un mode de programmation? 
  * un ensemble de concepts et d'outils mathématiques qui forment un modèle
  * un certain savoir-faire et un ensemble de méthodes -> génie (logiciel)

Dans ce contexte de génie logiciel, un programme ressemble à un "produit" dont on peut estimer (apprécier?) la qualité selon des critères tels que :
  * performance : temps de calcul, économie de mémoire, etc.
  * lisibilité : documentation, potentiel de réutilisation
  * correction : le critère le plus important.

Nous allons étudier les programmes selon trois aspects :
  - __sémantique du langage__ -- quel est la signification possible d'un programme dans le modèle considéré?
  - __preuve de correction__ par rapport à une spécification (ce terme reste à définir pour l'instant);
  - __la construction à partir d'une spécification rationnelle__ par des techniques de transformations successives.

Ce cours présente un modèle de raisonnement sur les programmes pour les construire, les transformer, les prouver.

==== Contexte ou difficulté de l'étude ====

Un programme est un texte qui relie deux univers de natures très différentes,
  * l'univers du problème "très descriptif", où la relation entre les données et le résultat est décrite, et
  * l'univers du programme, "très préscriptif", où les opérations à executer par l'ordinateur sont précisées.
C'est cette différence de natures qui nécessite l'introduction d'un modèle de raisonnement adapté.

=== Exemple ===

  * Problème : "trouver le nombre d'occurrences d'un nombre donné dans un tableau (ou liste) de nombres."
  * Données : ''t'', un tableau de ''n'' nombres\\ ''x'', un nombre
  * Résultat : le nombre ''p'' de fois que ''x'' apparaît dans ''t''

=== Enoncé qui qualifie le résultat ===

Ecrit de manière formelle, ce problème peut s'exprimer de la manière suivante, où l'on qualifie le résultat ''p''.

  * <jsm>\exists i_1 , \ldots i_p \in [0,\ldots ,n-1]</jsm> tels que
    * <jsm> \forall k\in [1,\ldots ,p] \quad t[i_k]=X </jsm>
    * <jsm>\quad\&\quad \forall i \in [0,\ldots ,n-1]\setminus \left\{i_1,\ldots i_p\right\} \quad t[i] \ne x</jsm>

=== Enoncé qui définit le résultat ===

Une autre forme d'énoncé permet d'exprimer ce problème et définit le résultat ''p'' au sens mathématique, c'est à dire que l'énoncé prend la forme "p=..." où ''p'' est définit cas par cas selon la valeur des données.

Dans le cas de notre décompte, la décomposition par cas repose sur la façon de construire le tableau et renvoie à la notion de type (quel est le type de ''t''?) et de constructeur (comment sont construites les valeurs de ce type?).

Supposons qu'un tableau est soit un seul élément, soit composé d'un élément et d'un tableau. Il nous faut une notation pour les valeurs des tableaux qui sont contruits. 

^ On notera : | ''a::t'' | le tableau à ''n'' éléments ou ''a'' est un élément et ''t'' est un tableau à ''n-1'' éléments. |

| p(a, x) = | 1  si '''x=a'' \\ 0 sinon |
| p(a::t, x) = | 1 + (t, x) si ''a = x ''\\ p(t, x) sinon |

Lorsqu'on définit le résultat (de façon explicite ou constructive) l'énoncé prend la forme d'une définition de fonction récursive (le résultat est fonction des données).  On peut se demander si cet énoncé est un programme ou non. Au sens stricte de prescription directe des opération à réaliser (par l'ordinateur), ceci n'est pas encore un programme. On peut simplement dire que cet énoncé prescrit indirectement les opérations à la manière des langages fonctionnels. Certains affirment que ces énoncés sont des spécifications et que le dernier énoncé est (sera) une "spécification exécutable."  Un "véritable" programme a plutôt la forme suivante (expression en langage C) :

  int
  occur (int * t[], int n, int x)
  {
  int i, p=0;
  for (i=0;i<n;i++) if (t[i]==x) p++;
  return p;
  }

Dans ce cours, on considère tous ces textes comme des énoncés en nous intéressant aux rapports de l'un à l'autre--suoit pour construire un programme, soit pour le prouver -- et on note simplement que ce dernier genre d'énoncé que l'on appelle programme impératif présente directement les instruction à exécuter par un processeur sur des données rangées en mémoire.

=== Exemple ===

  * Problème (ou énoncé descriptif) : suppression d'un nombre dans un tableau
  * Données : ''t'' un tableau, ''x'' un nombre
  * Résultat : ''u'' un tableau dans lequel ''x'' a été supprimé

Cet énoncé est imprécis. On peut, par exemple, préciser que le tableau ''u'' aura les mêmes éléments que ''t'' sauf ceux égaux à ''x''. Dans ce cas, on peut écrire l'énoncé qui qualifie le résultat :
  * ''u'' est un tableau tel que ∃ g une injection de [0, ... m-1] en [0, ... n-1] et 
    * ∀i∈ img(g) : t[i]≠ x,
    * ∀i∉ img(g) : t[i]= x,
    * ∀i∈ [0,...m-1] : u[i]=t[g(i)] 

Pour passer à un énoncé qui définit le résultat, on doit construire une injection g() qui satisfait à cette propriété. On peut en construire une en utilisant la fonction qui, à toute indice ''i'' associe le nombre d'éléments de ''t'' égaux à ''x'' et d'indice inférieur ou égale à ''i''.  Cette fonction, que l'on nommera //décale// est quasiment la même que dans l'exemple précédent: 

| decale(0) = | 1 si ''t[0] = x''\\ 0 sinon |
| decale(i) = | 1 + decale(i-1) si t[i] = x \\ decale(i-1)  sinon |

Illustration pour n=7 et x = 4 :

^ t          | 3 | **4** | 8 | 2 | 7 | **4** | 5 |
^ i          | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
^ decale (i) | 0 | 1 | 1 | 1 | 1 | 2 | 2 |

Ensuite, la fonction g() est définie à partir de la différence ''i - decale(i)''. Ces valeurs définissent le domaine de g() et étant donnée une indice dans ce domaine, g() associe l'indice du "prochaine élément de ''t'' différent de ''x''."

l'énoncé qui définit le résultat (en utilisant directement la fonction decale) sera :
  * ∀i∈[0,...,n-1], u[i-decale(i)] = t[i]
  * m = n - decale(n-1)

En C, cet énoncé peut être exprimé :

  int u[n];
  int
  suppress(int *t[], int *u[], int n, int x)
  {
  int i, p=0;
  for (i=0;i<n;i++) {
      if (t[i]!=x) u[i-p] = t[i];
      else p++;
      }
   return n-p;
   }

On peut préciser cet énoncé comme le ferait un programmeur dans un souci de'économie de mémoire en confondant les adresses mémoire de ''u[]'' et de ''t[]'', ce qui donne

  int
  suppress(int *t[], int n, int x){
  int i, p=0;
  for (i=0;i<n;i++) {
      if (t[i] != x) t[i-p] = t[i]; 
      else p++;
      }
  return n-p;
  }

==== Variables ====

On vient de voir une utilisation classique de la notion de variable dans ce que l'on appelle la programmation impérative.

La notion de variable en mathématiques est celle de l'inconnue dans une équation : résoudre l'équation donne une définition explicite. Par contre, en programmation impérative on peut trouver plusieurs définitions d'une même variable.

En informatique, //variable// est l'expression abstraite d'une adresse en mémoire.  Une définition est appelé **affectation** et signifie le rangement d'une valeur à cette adresse. One peut utiliser plusieurs fois la même adresse : cela a pour conséquence d'oublier la première valeur au profit de la seconde.  Cette notion de variable est évidemment dangereuse pour raisonner sur les programmes.  Elle interdit, par exemple toute substitution d'une variable par "sa" valeur alors que c'est la base même des mathématiques.  C'est ce qui justifie en grande partie ce cours pour introduire un modèle de raisonnement sur les programmes.

==== Modes de Programmation ====

=== Programmation Impérative ===


La programmation impérative est une programmation **par effet** parce qu'un programme est défini par son état sur un état mémoire.  La sémantique d'un programme est alors définie par une fonction appelée **fonction de transition entre états mémoire**

  * f:  état mémoire ''s'' tel que //conditions// -> état mémoire ''s' '' tel que //nouvelles conditions//

où  ''s'' et ''s' '' sont appelés respectivement état initial et état final.

La programmation impérative est fondée sur (et caractérisée par)
  * //variable// au sens informatique
  * //mode d'exécution// associé : transition d'état

N.B. Les types et les constructeurs sont aussi des éléments fondamentaux, mais qui ne sont pas spécifiques à ce mode, ils fondent aussi d'autres modes de programmation.

=== Programmation Fonctionnelle, Logique ===

Les autres modes de programmation utilisent des variables qui ont le même sens qu'en mathématiques. Dans ces modes, un énoncé est parfois une "spécification exécutable."

La programmation fonctionnelle est fondée sur (et caractérisée par)
  * fonction
  * mode d'exécution associé : réduction de λ-calcul

La programmation logique est fondée sur (et caractérisée par)
  * clauses de Horn
  * mode d'exécution associé : démonstration par réfutation((et jamais déduction? :?: Je ne sais pas, je ne connais pas ces langages.)) après unification nécessaire des termes.
----
A ceux-là on peut rajouter
  * des modes de programmation fondés sur des théories mathématiques éprouvées
  * des modes de programmation impérative atypique, qui posent des problèmes plus conséquents.

----
[[semantics_2|]] -0- [[semantics_td_1|]]