Documentation de programmes avec "displays"

Voir aussi :

• Parnas, D.L., Madey, J., Iglewski, M., "Formal Documentation of Well-Structured Programs", IEEE Transactions on Software Engineering, Vol. 20, No.12, 1994, pp.948-976.

• Un programme bien structuré peut être presque toujours présenté comme un texte court avec, éventuellement, des noms d'autres programmes dedans. Ces programmes nommés peuvent être aussi courts; ils peuvent contenir des noms de programmes plus simples.
• Un "display" est un document concis (1-2 pages) dans lequel un programme est présenté et lequel peut être analysé séparément de d'autres displays.
• Plus précisément, un display est composé des trois parties suivantes :
  • P1: la spécification du programme présenté dans le display,
  • P2: le programme lui-même, dans lequel des noms d'autres programmes (dits sous-programmes) peuvent apparaître; nous disons que des sous-programmes sont invoqués par ce programme,
  • P3: les spécifications de tous les programmes non-standard utilisés dans P2.
• Un programme standard est un programme qui n'exige pas une spécification; sa sémantique est déjà connue.
• Certains programmes non-standard peuvent exiger seulement une spécification - nous présumons qu'ils sont primitifs c.-à-d. leur implémentation est disponible et correcte.
• Si un sous-programme invoqué n'est pas standard alors sa spécification doit apparaître comme P1 dans un autre display.
• L'ensemble de displays pour un programme donné est considéré complet si pour chaque spécification d'un sous-programme non-standard trouvé dans P3 il existe un display dans lequel cette spécification constitue la partie P1.
• Un nom paraissant dans P2 peut être plus tard remplacé par un appel de procédure (dans ce cas la procédure doit être déclarée en suivant la spécification) ou bien il peut être traité comme appel de macro qui sera remplacé par une séquence d'instructions.
• Nous considérons qu'un display est correct si l'on peut justifier que P2 satisfasse P1 en présumant que les sous-programmes invoqués dans P2 satisfassent les spécifications P3.
• Chaque display peut être réexaminé sans aucune référence à d'autres displays; sa correction peut être vérifiée sans consulter l'implémentation de ces sous-programmes ou des programmes qui invoquent P2.
• Un sous-programme peut être invoqué dans plus d'un display. Pour éviter la répétition de la même spécification dans plusieurs displays, nous pouvons l'écrire une fois seulement - dans un document séparé dit le dictionnaire - et s'y référer dans les parties P3 de displays appropriés.

Exemple: recherche dichotomique

Définition du problème :

Une séquence de n entiers, a₁, ..., a_n, n ≥ 1, et un entier x sont donnés.

• Si les éléments sont dans l'ordre non-descendant, c.-à-d. a₁ ≤ ... ≤ a_n, nous voulons avoir un programme qui trouve une valeur quelconque j, 1 ≤ j ≤ n, telle que x = a_j, et qui aussi dit si une telle valeur j existe.
• Si les éléments ne sont pas ordonnés nous exigeons que le programme se termine (peu importe les valeurs finales des variables).

Discussion :

• La solution du problème sera présentée sous forme d'une fonction en Java et son invocation.
• La déclaration de la fonction sera précédée par des définitions et déclarations de constantes, types et variables que nous avons besoin pour définir la structure de données dont les valeurs formeront l'espace d'états.
• Nous prenons les décisions suivantes concernant la correspondance entre les concepts de la description informelle du problème et certains concepts du langage Java :
  • Des nombres entiers sont représentés par des valeurs du type standard int.
  • Le nombre d'entiers dans la séquence a₁, ..., a_n est représenté par la variable static final int n dont la valeur doit être initialisée à la longueur de cette séquence.
  • La séquence a₁, ..., a_n est représentée par la valeur de la variable A déclarée comme suit: int A[n];
  • Le nombre entier x est représenté par la valeur de la variable de int x.
  • Les résultats sont représentés par la valeur de la variable r de type Result, ce dernier défini comme suit :

    class Result {
      int index = 0;
      boolean found = false;
    }

• Nous spécifierons que :
  • Les valeurs de A et x ne peuvent pas être changées.
  • Si l'indice recherché existe alors r.index retournera sa valeur et r.found sera true.
  • Si l'indice n'existe pas alors r.found sera false et la valeur de r.index peut être changée de la façon arbitraire.
• Les observations et conventions suivantes se réfèrent à l'état de données :
  • Initialement l'état de données est composé des valeurs des éléments suivants : variables A, x et r.
  • La composante R de la LD-relation devra spécifier des changements acceptables de ces valeurs.
  • Pour les variables nous utilisons la convention 'v et v'.
  • Si v₁, ..., v_k sont des variables dont les valeurs ne devraient pas être changées alors nous pouvons abréger la notation dans la spécification par l'utilisation du prédicat standard NC ("not changed") défini comme suit :
    NC(v₁, ..., v_k) ⇔ (v₁' = 'v₁) ∧ ... ∧ (v_k' = 'v_k).
• Paramètres :
  • La spécification de l'invocation de la fonction sera écrite en fonction de paramètres effectifs.
  • Dans la déclaration de la fonction les paramètres formels seront utilisés.
  • Cela veut dire que les spécifications de sous-programmes apparaissant dans la déclaration et les instructions du corps doivent être écrites en fonction des paramètres formels de la fonction (et autres objets locaux ou pas).

  static class Result {
  int index = 0;
  boolean found = false;
  }
  public static void find(int e, int V[], Result res) {
    int low, high;
    initialization(); body()
  }

while (! res.found && (low <= high) ) {
  med = (low + high) / 2;
  test();
}

if (V[med] < e) low = med + 1;
else if (V[med] > e) high = med - 1;
else {
  res.index = med;
  res.found = true;
}

  low = 0;
  high = n-1;
  res.found = false;
  res.index = 0

Code de la fonction find après l'assemblage

  public static void find(int e, int V[], Result res) {
    int low, high;

    // initialization
    low = 0;
    high = n-1;
    res.found = false;
    res.index = 0;

    // body
    while (! res.found && (low <= high) ) {
      int med;
      med = (low + high) / 2;
      // test
      if (V[med] < e) low = med + 1;
      else if (V[med] > e) high = med - 1;
      else {
        res.index = med;
        res.found = true;
      }
    }
  }