TD10_invariant_boucle.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# TD - Terminaison et preuve d'algorithmes"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##  1. Terminaison : variant de boucle\n",
    "Expliquer ce que renvoie la fonction `mystere(a,b)`. On pourra pour cela prendre quelques valeurs de `a` et `b` :\n",
    "\n",
    "- Quand a=5 ; b=7   `mystere(5,7)` renvoie ............\n",
    "\n",
    "- Quand a=3 ; b=13   `mystere(3,13)` renvoie ............."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "def mystere(a,b):\n",
    "    ''' La fonction renvoie ???????\n",
    "    a et b : 2 integer'''\n",
    "    t = a\n",
    "    u = b\n",
    "    v = 0\n",
    "    while u>1:\n",
    "        if u%2 == 1:\n",
    "            v = v+t\n",
    "        t = t+t\n",
    "        u = u//2\n",
    "    return t+v"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `mystere` contient une boucle et pour être certain de toujours obtenr un résultat, il faut s'assurer que le **programme se termine**, c'est à dire qu'il ne reste pas bloqué indéfiniment dans la boucle.\n",
    "\n",
    "Pour **prouver** que c'est bien le cas, on peut utiliser un **variant de boucle**.\n",
    "\n",
    "Un **variant de boucle** est une quantité entière qui doit respecter deux conditions :\n",
    "1. elle doit décroitre à chaque itération,\n",
    "2. elle doit être positive ou nulle pour rester dans la boucle. \n",
    "\n",
    "Si l'on arrive à trouver un variant de boucle, il est évident que l'on va nécessairement sortir de la boucle au bout d'un **nombre fini d'itérations**, puisqu'un entier positif ne peut diminuer indéfiniment !"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Question :** Déterminer un variant de boucle permettant de prouver que l'algorithme  utilisé par la fonction `mystere` se termine en un nombre fini d'itérations.\n",
    "\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class = \"alert alert-info\">\n",
    "    \n",
    "**Exercice 1 :** Justifier en déterminant un variant de boucle que `appartient(val,tab)`, renvoyant `True` si la valeur `val` est présente dans la liste `tab`, est une fonction qui se termine.   "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "def appartient(val,tab):\n",
    "    '''la fonction renvoie True si val est dans tab\n",
    "    tab : liste non vide d entiers\n",
    "    val : un integer '''\n",
    "    i = 0\n",
    "    while i < len(tab) and tab[i] != val:\n",
    "        i += 1\n",
    "    return i < len(tab)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "................................................................................................................\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class = \"alert alert-info\">\n",
    "    \n",
    "**Exercice 2 :** La fonction suivante prétend calculer le nombre de chiffres d'un nombre entier positif saisi par l'utilisateur. \n",
    "\n",
    "1. Exécuter la fonction pour `n=9` et `n=9999`\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "2. Identifier un variant de boucle. Que peut-on conclure sur la terminaison de la fonction ?  \n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................\n",
    "\n",
    "................................................................................................................"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "4"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def nb_chiffres(a):\n",
    "    k = 1\n",
    "    i = 0\n",
    "    while k != a+1:\n",
    "        k = k*10\n",
    "        i += 1\n",
    "    return i\n",
    "nb_chiffres(9999)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 2. Correction d'un algorithme : invariant de boucle\n",
    "\n",
    "Quand un programme contient des boucles, il est important de se poser les questions suivantes : \n",
    "\n",
    "- les variables sont-elles correctement initialisées avant la boucle ?\n",
    "- le nombre de tours de boucles est-il le bon ?\n",
    "- les valeurs obtenues en sortie de boucle sont-elles les bonnes ?\n",
    "\n",
    "**Un invariant de boucle** peut nous aider à comprendre pourquoi un algorithme est **correct**. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Définition d'un invariant de boucle** c'est une proposition qui doit vérifier 3 conditions :\n",
    "1. Elle est VRAIE **avant** d'entrer dans la boucle (**initialisation**)\n",
    "2. Elle reste VRAIE **après** une itération (**conservation**)\n",
    "3. Elle donne le résultat attendu en fin de boucle (**terminaison**)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Exemple de la validité de l'algorithme du tri par insertion**\n",
    "\n",
    "Nous avons largement étudié ce tri dans les TD précédents, l'objectif est maintenant de prouver sa coorection.\n",
    "\n",
    "Rappelons l'algorithme et le principe sur un exemple :\n",
    "\n",
    "```\n",
    "Pour j variant de 1 à len(t)-1:\n",
    "    c prend la valeur t[j]\n",
    "    i prend la valeur j-1 \n",
    "    Tant que i>=0 et c<t[i]:\n",
    "        permuter t[i] et t[i+1]\n",
    "        i prend la valeur i-1\n",
    "    fin Tant que\n",
    "    t[i+1] prend la valeur de c\n",
    "fin Pour```\n",
    "\n",
    "![selection](insertion.png)\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On choisit comme **invariant de boucle** la proposition __P(j) : \"A la fin d'un tour de boucle Pour, les valeurs de la liste sont triées jusqu'à la case j incluse\"__"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "1. **Initialisation** Au début, avant d'entrer dans la boucle, **j vaut 0**. La liste est réduite à un unique élément d'indice 0, elle est donc triée. **P(0) est VRAIE.**\n",
    "2. **Conservation** On se place à la fin de l'itération __j__. La liste est donc supposée triée jusqu'à l'indice j inclus (**P(j) est supposée VRAIE**). On effectue un nouveau tour de boucle, donc on se place à l'itération **j+1** :\n",
    "    - c prend la valeur t[j+1]\n",
    "    - i prend la valeur j\n",
    "    - Tant que i>=0 et c<t[i+i]:\n",
    "    -    permuter t[i+1] et t[i]\n",
    "    -    ...\n",
    "    - la liste est donc triée jusqu'à l'indice __j+1 inclus__. **P(j+1) est VRAIE**\n",
    "3. **Terminaison** En sortie de boucle, __j__ a pris sa dernière valeur __len(t)-1__ c'est à dire l'indice de la dernière case et on a montré que la liste était triée jusqu'à cette case. **La liste est donc entièrement triée**. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "    \n",
    "__Exercice 3:__ Donner un invariant de boucle pour la fonction suivante :\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "def power(x,n):\n",
    "    '''La fonction renvoie x à la puissance n\n",
    "    x : un float\n",
    "    n : un entier positif'''\n",
    "    r = 1\n",
    "    for i in range(n):\n",
    "        r = r * x\n",
    "    return r"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "...................................................................................................................\n",
    "\n",
    "...................................................................................................................\n",
    "\n",
    "...................................................................................................................\n",
    "\n",
    "...................................................................................................................\n",
    "\n",
    "...................................................................................................................\n",
    "\n",
    "..................................................................................................................."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "    \n",
    "__Exercice 4:__ La fonction itérative `facto(n)` suivante calcule et renvoie la valeur de $n!$ (factorielle n) pour un entier `n` telle que $n! = 1 \\times 2 \\times 3 \\times \\cdots \\times n$ :\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [],
   "source": [
    "def facto(n):\n",
    "    res = 1\n",
    "    for i in range(2,n+1):\n",
    "        res = res * i\n",
    "    return res"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "    \n",
    "**Question 1 :** Quelles sont les préconditions de cette fonction ?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    ".........................................................................................................."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "    \n",
    "**Question 2 :** Démontrer la terminaison de cette fonction."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    ".................................................................................................................\n",
    "\n",
    ".................................................................................................................\n",
    "\n",
    "................................................................................................................."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "    \n",
    "**Question 3 :** Montrez que la proposition **P(i) : \"A la fin du tour de boucle i, res prend la valeur $i!$ \"** et démontrez la correction totale de la fonction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    ".................................................................................................................\n",
    "\n",
    ".................................................................................................................\n",
    "\n",
    ".................................................................................................................\n",
    "\n",
    ".................................................................................................................\n",
    "\n",
    ".................................................................................................................\n",
    "\n",
    ".................................................................................................................\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "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.7.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}