Stagiaire_preuve_terminaison.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Preuve de terminaison"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Table des matières\n",
    "**[Chapitre 0 - Rappel de la position du problème](#M0)**\n",
    "\n",
    "**[Chapitre 1 - Variant de boucle](#M1)**  \n",
    " \n",
    "**[Chapitre 2 - Théorème (Terminaison d’une boucle, d’un algorithme)](#M2)** \n",
    "\n",
    "**[Exercice 1](#M3)**\n",
    "\n",
    "**[Exercice 2](#M4)**\n",
    "\n",
    "**[Exercice 3](#M5)**\n",
    "\n",
    "**[Exercice 4 (programme première NSI)](#M6)**"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Chapitre 0 - Rappel de la position du problème</font> <a name=\"M0\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Lorsqu'on écrit un programme il est parfois très important de vérifier qu'il est correct, c'est à dire qu'il calcule bien ce qu'on attend. C'est même vital lorsque dans certaines applications industrielles une erreur aurait un impact sur des vies humaines (on pensera par exemple aux programmes qui contrôlent la conduite des lignes de métro automatiques, ou à des programmes touchant au secteur militaire).\n",
    "Si la preuve - automatique ou non - de programmes est un vaste sujet où la recherche est active aujourd'hui, elle dépasse en général le cadre et le formalisme de ce cours. Néanmoins, un cas particulier nous est accessible : il s'agit de la preuve de la correction de boucle."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "De manière plus détaillée, nous allons :\n",
    "* Montrer qu'une boucle se termine bien. On appelle ce problème la <b>*terminaison*</b>.\n",
    "* Montrer que si la boucle s'arrête, elle calcule bien ce qu'elle est supposée calculer. On appelle ce\n",
    "problème la *correction partielle*.\n",
    "* La *correction totale* est la <b>*terminaison*</b> et la *correction partielle*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Un algorithme est un programme de calcul qui s'exécute en un nombre fini d'étapes. Si dans le cadre des boucles inconditionnelles on a la certitude que le calcul se finira effectivement, lors de l'exécution d'une boucle conditionnelle, nous n'avons pas cette certitude.\n",
    "Considérons par exemple le programme suivant :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "c=int(input())\n",
    "p=1\n",
    "while c > 0:\n",
    "    p = 2*p\n",
    "    c = c-1\n",
    "print(p)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Ce programme calcul $2^{c}$ au moyen d'une boucle. La variable c joue le rôle d'un compteur lors de l'exécution de la boucle. Comme c est strictement décroissante lors de l'exécution de celle-ci, ce programme s'arrêtera après c étapes.\n",
    "Regardons maintenant une variante de ce programme :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "c=int(input())\n",
    "p=1\n",
    "while c != 0:\n",
    "    p = 2*p\n",
    "    c = c-1\n",
    "print(p)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Ce programme comporte un problème de taille : si l'utilisateur rentre un nombre négatif lors de la saisie de c, la condition c != 0 ne sera jamais vérifiée (ce qui explique que le premier programme soit correct là où le second ne l'est pas) et ce programme ne s'interrompra jamais. Ceci s'appelle une boucle infinie. Ce type d'erreurs de conception est indétectable par l'ordinateur et il est en pratique assez courant car les conditions de sortie de boucles sont souvent plus complexes que dans cet exemple. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Dans l'exemple précédent, la variable c joue le rôle d'un compteur. Cette variable diminue de 1 à chaque itération et la boucle s'arrête lorsqu'elle n'est plus strictement positive. En généralisant, une quantité qui vérifie certaines propriétés sera appelé un variant de boucle et permettra de montrer la terminaison d'un programme."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Chapitre 1 - Variant de boucle</font> <a name=\"M1\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les variants de boucle sont un outil qui va permettre de montrer la *terminaison* d'algorithmes.\n",
    "#### Définition  (variant de boucle).\n",
    "Un variant de boucle est une quantité entière définie en fonction des variables ($x_1$, . . . , $x_k$) constituant\n",
    "l’état de la machine, et de n, le nombre de passages effectués dans la boucle qui :\n",
    "1.\test un entier strictement positif avant l'exécution de la boucle\n",
    "2.\tdécroît strictement à chaque itération\n",
    "3.\tlorsqu'elle est inférieure à un certain nombre (en particulier lorsqu'elle arrête d'être strictement positive) rend la condition d'exécution de la boucle conditionnelle fausse"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Chapitre 2 - Théorème (Terminaison d’une boucle, d’un algorithme)</font> <a name=\"M2\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "1. Si, pour une boucle donnée, on peut exhiber un variant de boucle, alors le nombre de passages\n",
    "dans la boucle est finie.\n",
    "2. Si, pour un algorithme donné, on peut exhiber, pour toute boucle de l’algorithme, un variant de\n",
    "boucle, alors l’algorithme s’arrête en temps fini"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Remarque :\n",
    "Dans le cas d’une boucle for, on peut toujours construire un variant simple. Si la boucle est donnée\n",
    "par la structure :\n",
    "Pour i ← a à b,\n",
    "un variant simple est b − i"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les variants de boucles sont des outils puissants pour étudier la terminaison d'une boucle ou d'un algorithme. Néanmoins il est parfois difficile d'en exprimer, et à l'heure actuelle on ne sait pas si certains programmes de calcul d'apparence simple (par exemple la suite de Syraccuse) s'arrêtent effectivement."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Exercice 1</font> <a name=\"M3\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On donne la fonction suivante (déjà vue par ailleurs). Les variables $\\texttt{x}$ et\n",
    "$\\texttt{n}$ sont de type entier."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def Mystere(x,n) : # x et n sont des entiers\n",
    "    res=1\n",
    "    while n>0 :\n",
    "        if n%2==1 :\n",
    "            res=res*x\n",
    "        n=n//2\n",
    "        x=x*x\n",
    "    return res"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Prouver la terminaison de cette fonction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Exercice 2</font> <a name=\"M4\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On considère le programme (déjà vu par ailleurs) :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def somme_liste(T, S):\n",
    "    '''partant d’une liste T, on détermine si la somme des éléments de T\n",
    "       est ou non supérieure à une valeur entière donnée S.\n",
    "       Entrez votre fonction ici'''\n",
    "    N = len(T)\n",
    "    i , sss , sp = 0 , False , 0\n",
    "    while not(i == N):\n",
    "        sss = sss or (sp + T[i]>S)\n",
    "        sp = sp + T[i]\n",
    "        i += 1\n",
    "    return sss"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Prouver la terminaison de cette fonction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Exercice 3</font> <a name=\"M5\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On considère le programme (déjà vu par ailleurs) :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def somme_indice(T, S):\n",
    "    '''partant d’une liste T, on détermine si la somme des éléments de T\n",
    "     est ou non supérieure à une valeur entière donnée S et si oui à partir de quel indice c'est la cas.\n",
    "     Entrez votre fonction ici'''\n",
    "    N = len(T)\n",
    "    i , sp = 0 , 0\n",
    "    while not((i == N)or (sp + T[i]>S)):\n",
    "        sp = sp + T[i]\n",
    "        i += 1\n",
    "    sss = not(i == N)\n",
    "    return sss, i"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Prouver la terminaison de cette fonction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <font color=#3876C2> Exercice 4 (programme première NSI)</font> <a name=\"M6\"></a>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On considère la fonction suivante :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "import math"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def ex4(T, V) :\n",
    "    '''T est une liste triée de manière ascendante\n",
    "    et V un entier naturel'''\n",
    "    N = len(T)\n",
    "    i, s = 0, N-1\n",
    "    while not(i == s) :\n",
    "        m = int(math.floor((i + s)/2))\n",
    "        if T[m] < V :\n",
    "            i = m + 1\n",
    "        else :\n",
    "            s = m\n",
    "    return T[i] == V\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "ex4([1, 2, 6, 8, 12], 8)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Que fait-elle ?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Réponse : \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<figure>\n",
    "\n",
    "<center><figcation>Extrait du programme NSI première</figcation></center>\n",
    "</figure>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*assertion = prédicat en logique propositionnelle*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Déterminer sa spécification"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Réponse :\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Prouver sa correction "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Réponse : "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Prouver sa terminaison."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Réponse : \n"
   ]
  }
 ],
 "metadata": {
  "hide_input": false,
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}