129 lines
294 KiB
Plaintext
129 lines
294 KiB
Plaintext
|
{
|
|||
|
|
"cells": [
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"source": [
|
|||
|
|
"# Annexe optionnelle — Preuve et complexité de l'algorithme de Dijkstra\n",
|
|||
|
|
"VERSION ELEVE\n",
|
|||
|
|
"\n",
|
|||
|
|
"> **Cette annexe est facultative.** Elle prolonge la Séance 6 pour les étudiantes à l'aise et curieuses d'aller plus loin dans la formalisation (preuve d'algorithme, complexité). Elle n'est pas nécessaire pour suivre la Séance 7 (implémentation) ni pour l'évaluation."
|
|||
|
|
],
|
|||
|
|
"metadata": {}
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"## 3- Preuve de l'algorithme de Dijkstra\n",
|
|||
|
|
" #### Rappel de cours sur la preuve d'un algorithme: \n",
|
|||
|
|
" réaliser la preuve (appelée aussi \"correction totale\"$*$) d’un algorithme, par deux vérifications :\n",
|
|||
|
|
" • Prouver (vérif.1) sa terminaison .\n",
|
|||
|
|
" • Prouver (vérif.2) sa correction (appelée aussi \"correction partielle\"$*$).\n",
|
|||
|
|
" #### Terminaison (vérif.1) : \n",
|
|||
|
|
"Consiste à vérifier que les calculs effectués par l’algorithme s’arrêtent bien.\n",
|
|||
|
|
"Notamment, lorsqu’une boucle conditionnelle est effectuée par l’algorithme, il est primordial de\n",
|
|||
|
|
"vérifier que l’on sort bien de cette boucle, en particulier si cette boucle est non bornée. Dans ce dernier cas, identifier un variant de boucle (quantité entière positive ou nulle) qui doit décroitre à chaque itération."
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"### Travail à faire 3, \"preuve\" de l'algorithme de Dijkstra: terminaison\n",
|
|||
|
|
" Montrer la terminaison de cet algorithme en raisonnant sur son écriture (proposée au Taf2). Pour cela, répondre au QCM2 ci-dessous."
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"$QCM2:$ Dans l'écriture de l'algorithme de Dijkstra proposée au Taf2, pour montrer sa terminaison, on peut raisonner comme suit:\n",
|
|||
|
|
" $Rep1:$ La boucle conditionnelle 'Pour' porte sur le parcours des sommets voisins, donc la variable $s_{voisin}$ est le variant de boucle. A chaque itération, le plus proche sommet voisin est mis à jour. Donc quand tous les sommets ont été parcourus, l'algorithme donnera le plus court chemin. \n",
|
|||
|
|
" $Rep2:$ Dans cet algorithme, il y a une boucle conditionnelle non bornée, donc cela suffit pour montrer sa terminaison.\n",
|
|||
|
|
" $Rep3:$ La boucle conditionnelle non bornée 'Tant que' porte sur la condition du parcours exhaustif des sommets du graphe pondéré, donc la variable $E_{calculés}$ est le variant de boucle. A chaque itération, le sommet actuel de poids minimal est ajouté à $E_{calculés}$. Donc pour $n$ sommets, et en autant d'itérations, tous les sommets auront été parcourus et l'ensemble $E_{calculés}$ sera rempli. \n",
|
|||
|
|
" $Rep4:$ La boucle conditionnelle non bornée 'Tant que' porte sur la condition du parcours exhaustif des sommets du graphe pondéré, donc la variable $E_{sommet}$ est le variant de boucle. A chaque itération, le sommet actuel de poids minimal est retiré de $E_{sommet}$. Donc pour $n$ sommets, et en autant d'itérations, tous les sommets auront été parcourus et l'ensemble $E_{sommet}$ sera vide. "
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"#### Suite du rappel de cours sur la preuve d'un algorithme, Correction (vérif.2) : \n",
|
|||
|
|
" Consiste à prouver que l’algorithme aboutit au résultat escompté en identifiant un \"invariant de boucle\". Cet invariant doit posséder une propriété vérifiable avant l’entrée dans la boucle, lors d'une itération n de la boucle, ainsi qu'à l'itération n+1 et enfin amène au résultat escompté à la sortie de la boucle."
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"attachments": {
|
|||
|
|
"Algo_Dijkstra_f_secondaires_f2_non_comment%C3%A9es.png": {
|
|||
|
|
"image/png": "iVBORw0KGgoAAAANSUhEUgAABH8AAAONCAIAAACQtFtJAAAAAXNSR0IArs4c6QAAAARnQU1BAACxjwv8YQUAAAAJcEhZcwAADsMAAA7DAcdvqGQAAP+lSURBVHhe7J0FYBRHF4D3JO5uxENcIEIIFoJrcXeHFgqUUqBYofSHAsW9WHELbsUSEmIkIW7EQ9yTc/9393bPYncRoO183XKbubnZ0TfvzczOEAQCAQQAAAAAAAAAAAAAgC6GiH0CAAAAAAAAAAAAAKArAdYXAAAAAAAAAAAAAHwOgPUFAAAAAAAAAAAAAJ8DYH0BAAAAAAAAAAAAwOcAWF8AAAAAAAAAAAAA8DkA1hcAAAAAAAAAAAAAfA5a2nGeV/7k59V/ZrGwP1tCzeunMzv6aGF/fXVwGyqZmsaaJOxPdsGNn9bfKODAt8oO8w/uGW9BFn4B+EppeLd9+f4kBnxHMh6x88hyN1Whu7yAEgcAAAAAAAAAfEW0ZH1xcw54d1+Xgv3VMn2uVkbMNML++JpgFf198McfTnL3JN4dq4e5MRN+dvPenYfeO+9KS9zsqoLeA75WKq/0MZkThd4aznuTdzFIQUMflDgAAAAAAAAA4Cvi37jykFv6bMc3LrYjNt1Or+ZibgAAAAAAAAAAAADwZZFr7stg8PzJDs1OGqi6LNm12kcT++srofbuUNNJr5DVZpD62IfFD0VzX+zciytWXMxlw7cqTsv/PD7dCqxD+7rp6NwXKHEAAAAAAAAAwFeEXNbXV7u8sHlatL4A/zQ6an0BAAAAAAAAAABfEZ1uffHqUx9dvBj8MiajqIZB1jaxcgsYMWXBnGEOmlKLHLklzw4de1PBhSCyyaCVa0YaVry9dOxscHh6SSNB385n6LSl30710ce3yxDBb0h7eP5C8Kv3mcXVNIG6QTcnn6CJCxaP99ITemVmXvn9fEzi9WP3i9G/IZsJqybbqyjbTlm/vJcuv+zl4SMvypHViErdxqxZGWgs+YAujDmzMOTy2WvPolLzy2rpPLK6rom1i2/QxPnzR7vqyLf2U6EQ+JSMh2dO33j+/mNZo0DD2Nqz/5hZi+cMtGxu+rKtHJVCvixqZ9nyqt5fPXbmdkhiYR1f29p76KxVq6eaPe7fkvXFKgm7eubq06iU/LI6KoeopmPUrXvPwAkLloz31BWFzW22xJmZl/ecT6bBFV/Ffvr6OVp//7b52POPdG373uOXrV8+3BrZ2kP+POx44QIAAAAAAAAA/ivA1ldzcLL/8MB8oNYX5tw6tIxLS7zUsB9JYTBg09NSDuYNgfZ+nTX2nfWah9e/69FEqzUccyKDiflG4RQ/+tFfG/tWCu2+m19XcBE/tQ/HqmOOUvicLIS/Z3zYZIc5IHswSITehTFn5l6Z50DAvpLBZMzhJCrmr2UUCoFXE/Hb0GYsZYLd1FMpMs+SJ0dFyJ9F7ShbbmXI1r5NYmI8atvPPbB7xPpqxHwLOEXBy1xbWEOoP+T32EYe5rH5Eq99MBpPiM+v+ycYYPcwRgteww+RPw87XrgAAAAAAAAAgP8QcllffqczK5pSWUuT1M9ZuefH6WM/aBareXdKRDq6hIYO6bbw3pjqkL+K8Sfwal6v6o65N4fGkJM5rHZaX10Zc2ba777iWR4VY1tHJwcLyeVzdqvDRUZFsygUAi359z7NzXAJ0R9/qUCUDjlzVIhCWaRo2QqYGYcD29xKXmx9sXKOB7acSBivPelYzNu0viAl7BPFbGkYRYE87HjhAgAAAAAAAAD+U8hlfbWA5PQRp+DCcA3MHYK0/FccexSVnBz18MhSX7Gz9tgruMotqaHDWIzf8yyXwuM2pl6aJ3ZXGR5cg3mP3Si2FAyGbgtOKKmvK467tsZXpCcbzn1RJ2AVPj9/Yt8yR8wNIrp/u//48eNn7qYjsxDN6uJdGnNm0jY8LgZTbxRiNgGn/MWP7tiiNJLD8pB6oXOzKBICJ/dEf5E1YTHpSEQZS8Cp+XB2ngPmBhnOfqpgjiIomEUKli2v8sFkXcwVNteCtj3KpvB4tIJXu0cbY44IIuuLGrmqG+YGWc39K7UefiqXkn1vtTPmCBH7XS4Tzn61bX3BKDmPX7X551WTA/r+FEVVIA87XrgAAAAAAAAAgP8WnWR9MRK2iCweUs8dcRIrrhqjN7th30CQ47ZEBuoqpaHbro8R/YBXfmO4aB7EY38WOs9AebvYFHOCTBe9rMUXlglY6bvdYTftbu59v1l9LVeoANcED8H1Z/WxD2tRN5TmdPGujTkldBFuQSh5r73+oQJT0QXUzMe3HkWkl9NESWkBBUJgpv3minmFzJeFitV+Wtwm3HbQGBOMriJVJEcVzSLFylZQc/8bkQ1nPP9ptThH6kOWW2BfSFhfPGpJcui9Cwe3rVm1O6xG5JuTc9AT8wq5/JYmzCY5rC/96ffKxY9UKA87XLgAAAAAAAAAgP8WnbMtADv/2d2P2L3WmK0rfMRTIpCW38otw3Cd++Pdl4XYrRiTQaNdRT8gatm5m2D3EIvC4iEfhWHvyoUukMGwmf56olgrO615W8vgNXxKeffg0Aw7ZcxZfro45qpW3jbYa0GcDwdneJtomnkOnrFq56kXde6jRvVxMVFvqwDkD4FfG/8sC7vX8h/rpYPdwzao06jBZsJbWtzfmVTFcrRDWdRmDkH0vMgUGuoC24HjF/Y3EOeIjt+c8WLzC4eoYe4ROH7+mh0Hj2zsr0+E2DVZEfdO71z1/ckMzAfEZXH52G1bGI5dMthE9EhF8rATChcAAAAAAAAA8N9CLv3Q52hiQVMKQ753xFap0QsTSoR3EGQb6CG9wztRz6O/DXYPlSZhmxFKoGttKPH2DUlNW7T2DbEP4Q92RXa10AGCjLqbSNpYRFV9PdUOKLldHHOy9bSdS0VBwHDKU97cOLZ9xcQAG00z3xk77+fglkcLyB8Cu+JjOWrPwFDujTdVE2M46HQZ9k1lehHsX5Ec7VAWtZlDEKemsA51gDF17yaaG0NQs/TCLB5Z2JWxN39fNTnQ1VRFxdC538Tl2089/YgeMoAA20QtbIXRBIueNhKrEBXJw04oXAAAAAAAAADAfwu5DBcVfXPrpliZaom2neNxcZ0VUtZUkQmUpKopUu+5DBZ2J0ZZQ0W8dwEcJZJspPgcFrJnuBCCvHq1fHRtzCGiwfAj757+Mt65mc1AKuNvbJ/gMWx3Eh1zaBa5Q+CzGSLzA5n+YYphib/gU2vpXMVytCNZ1HYOCXhsUfBEonRciCpqErYbDrf0wSo/y17TNx4LDsuoQE5ShiBVix79vcWbJjZ9TAsQtIzFtVixPOyMwgUAAAAAAAAA/KeQV0ttHSU9c9EarZqcCiZ2i8GqyKnBbiEdS4n9vTEIban/ZC1D0eq1hk+1EvoxBLHrSiqoIvVdYbo45gjKFiO338uoLYu9e2TTglG+NtK7ADIjf934uKL1dXLyhUDWMhDlku6I/1251Sx3D4wyJiuUox3KorZziKxlJEpPfXGNdFRqihuwWxG80jvL5xxLFhpdWr7zf734PLGURiuOu7JEtI0IbMVhd22hpK4qaR0qkocoHS9cAAAAAAAAAMB/h86xvtTs+7rgMyD59+5nSY3301KCH+NL1zS9B4r2jpMfNRs/O3yCoiw8rEhihqUhbLWXqRZZzaS778ifXtVgiq5I5Rfwmz1LWkwXxxyGSylNj/47+GGmyehV/zv/JDafwqxMe3lqmQeeIkZGTKGMSSONnCEom3k547M/NLp50KQpIkb3sjR18B0yDr6dEGQP2xeK5GhXF661rxVeXPmvo0rFc3IQr+zdk2zsXkRN2JnnFOGt7uQrz89tmTfcy0ydCOdSFfIyFgpBZg6tZUhkKUNNkTxE6HjhAgAAAAAAAAD+Q3SO9UU0HLhwML78Knv3rA0PPwnnJiBW4d11cw/gmzEYT14Z2HQGqU2IxgNm+OFTFOm/rzubir1PQ0s++8stZOqFWZkTn6diqIEmh0BSxj2zGxtZrU49dG3MKaFLrZW0LdwCRkyeOnPHG8w4VDFyHTL/2wmizfhUdTUk51+kUCQEbd8ZAzCr
|
|||
|
|
}
|
|||
|
|
},
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"### Travail à faire 4, \"preuve\" de l'algorithme de Dijkstra: correction\n",
|
|||
|
|
"L'algorithme détaillé des trois fonctions secondaires, de l'algorithme de Dijkstra proposé au Taf2 vous est donné ci-dessous. \n",
|
|||
|
|
" Vous admettrez que $poids[s_{voisin}] ≥ poids[s_{mini} ] + Distance(s_{mini} , s_{voisin}) )$ est un invariant de boucle dans cet algorithme et qu'il est vérifiable à chaque itération de la boucle principale dans l'algorithme de Dijkstra .\n",
|
|||
|
|
" 1- Que signifie l'affirmation (démontrée) ci-dessus pour la correction de cet algorithme?\n",
|
|||
|
|
" 2- Conclure sur la preuve de l'algorithme de Dijkstra.\n",
|
|||
|
|
" "
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"## 4- Complexité de l'algorithme de Dijkstra\n",
|
|||
|
|
" ### Rappel de cours, complexité (temporelle) d'un algorithme\n",
|
|||
|
|
"Le calcul de la complexité d’un algorithme permet de mesurer sa performance. Il en existe deux types :\n",
|
|||
|
|
" - complexité spatiale : permet de quantifier l’utilisation de la mémoire\n",
|
|||
|
|
" - complexité temporelle : permet de quantifier la vitesse d’exécution\n",
|
|||
|
|
" Réaliser un calcul de complexité temporelle d'un algorithme revient à compter le nombre d’opérations élémentaires (affectation, calcul arithmétique ou logique, comparaison…) effectuées par cet algorithme. On calculera le plus souvent la complexité dans le pire des cas, car elle est la plus pertinente. \n",
|
|||
|
|
" Pour simplifier on s'interresse à l’ordre de grandeur (asymptotique), noté O (« grand O ») du calcul exact exhaustif (qui peut être complexe) consistant à négliger le nombre d'instructions éxécutées en 1 tour de boucle (en le ramenant à 1) devant n (nombre de données à traiter) tours de boucle (soit n tours dans une boucle 'Tant que').\n",
|
|||
|
|
" Pour repère,quelques valeurs: \n",
|
|||
|
|
" pour un nombre n de données à traiter, l'ordre de grandeur de la complexité d'une boucle simple est O(n), de k boucles consécutives est k x O(n) et pour deux boucles imbriquées est O(n x n) = O(n²) ."
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"### Travail à faire 5, complexité (temporelle) de l'algorithme de Dijkstra\n",
|
|||
|
|
" Déterminer l'ordre de grandeur de complexité de la version proposée de l’algorithme de Dijkstra en portant attention à l'agencement des boucles dans cet algorithme. Pour cela, répondre au QCM3 suivant."
|
|||
|
|
]
|
|||
|
|
},
|
|||
|
|
{
|
|||
|
|
"cell_type": "markdown",
|
|||
|
|
"metadata": {},
|
|||
|
|
"source": [
|
|||
|
|
"$QCM3:$ Dans l'écriture de l'algorithme de Dijkstra proposée au Taf2, la fonction principale contient des boucles et pour déterminer sa complexité (en ordre de grandeur), on raisonne comme suit:\n",
|
|||
|
|
" $Rep1:$ Une boucle non bornée de complexité $O(n-1)≈ O(n)$ et une boucle bornée de complexité $O(n-2)≈ O(n)$ , toutes deux consécutives d'ou une complexité $2×O(n)$.\n",
|
|||
|
|
" $Rep2:$ Deux boucles bornées imbriquées, d'ou une complexité $O(n × n) = O(n²)$.\n",
|
|||
|
|
" $Rep3:$ Une boucle 'Pour' de complexité $O(n-1)≈ O(n)$ imbriquée dans une boucle 'Tant que' de complexité $O(n-1)≈ O(n)$, d'ou une complexité $O(n × n) = O(n²)$.\n",
|
|||
|
|
" $Rep4:$ Une boucle 'Tant que' de complexité $O(n-1)≈ O(n)$ consécutive à une boucle 'Pour' de complexité $O(n-1)≈ O(n)$, d'ou une complexité $2×O(n)$"
|
|||
|
|
]
|
|||
|
|
}
|
|||
|
|
],
|
|||
|
|
"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.6"
|
|||
|
|
}
|
|||
|
|
},
|
|||
|
|
"nbformat": 4,
|
|||
|
|
"nbformat_minor": 4
|
|||
|
|
}
|