Ce que j'ai fait lors du deuxième cours

Ce matin de 8h 15 à 9 h 15

- Les axiomes des substitutions :

• skip
• préconditionnée
• gardée
• choix indéterministe

ainsi que les cas pathologiques : le crash, le miracle.
(voir l'accident du premier "vol" d'Ariane IV pour exemple de crash : non respect de précondition)
http://www.mines.inpl-nancy.fr/~tisseran/cours/qualite-logiciel/qualite_logiciel.html
Gilles Kahn, co-auteur du rapport

"Premier vol (vol 88 / 501) [modifier]

Le premier tir eut lieu le 4 juin 1996 à Kourou, mais le lanceur fut détruit après approximativement 40 secondes de vol. L'échec était dû à une erreur informatique (bogue), un programme d'un composant (un gyroscope) provenant d'Ariane 4 n'ayant pas été re-testé.^[1]

L'erreur

La conversion d'un nombre flottant de 64 bits vers un nombre entier de 16 bits dans un logiciel en Ada provoqua un dépassement de mantisse. La routine de gestion de cette erreur avait également été supprimée pour des raisons de temps d'exécution ; sur Ariane 4 on pouvait prouver que l'occurrence d'un tel dépassement était impossible compte tenu des trajectoires de vol possibles. Toutefois les trajectoires de vol envisageables avec Ariane 5, notamment en phase de décollage, diffèrent notablement de celles d'Ariane 4. Le programme du composant concerné, pourtant lui-même redondant (deux gyroscopes sont présents dans la cellule de la fusée), déclencha donc successivement deux dépassements pour finir par signaler sur les sorties du système la défaillance des systèmes gyroscopiques. De toute façon, le gyroscope étant un système critique, le calculateur de pilotage de la fusée (lui conçu spécifiquement pour Ariane 5) ne tenait pas compte de ce signal d'erreur ! Il interpréta donc les valeurs d'erreurs (probablement négatives) du deuxième gyroscope comme une information d'attitude (indiquant probablement que, brutalement, la fusée s'était mise à pointer vers le bas). La réaction du calculateur de pilotage (braquer les tuyères au maximum pour « redresser ») augmenta considérablement l'incidence du lanceur (angle entre le vecteur vitesse et l'axe du lanceur), ce qui provoqua des efforts aérodynamiques suffisants pour détruire le lanceur ^[2]. Il s'agit certainement là d'une des erreurs informatiques les plus coûteuses de l'histoire ^[3].

Le programme en question était destiné à recalibrer les gyroscopes dans le cas d'un court retard de tir (quelques minutes) pour permettre une reprise rapide du compte à rebours - par exemple en raison de variations rapides des conditions météo du site de lancement à Kourou. Ce cas de figure, envisagé initialement pour Ariane 3, était depuis longtemps exclu des procédures de tir. L'erreur en question a donc aussi été provoquée par un programme qui ne servait à rien. "

source : Wikipedia

Si vous désirez le rapport d'enquête complet, me faire signe.

- Rappel de la notation pour les relations, fonctions

- Analyse du proverbe
" Qui que saille notre jument, le poulain est notre."

J'ai spécifié le "Qui que"
le "saille"
le "notre jument"
le "est notre"
"a pour mère"
"a pour père"

J'ai tenté de faire comprendre que si on spécifiait des fonctions totales pour "a pour mère" et
"a pour père", étant donné ce que nous n'avions pas spécifié mais que vous savez : un père ne peut être son propre père et si a est père de b et b père de c, c ne peut être père de a (voir votre cours sur relations d'ordre), nous avions des ensembles infinis. Bonne occasion pour revoir votre cours de philo ou de religions comparées.