Discussion :

[kaukau]

Bonjour,
dans une optique preuve de programmes (prouver qu'on est conforme à une spec), je me suis fait les réflexions suivantes:

Embarquer la précision

Lorsque je travaillais pour la marine, nous avions un simulateur maritime justement, dans lesquels les bateaux, au bout d'un certain temps... Volaient à quelques mètres au dessus de l'eau!!
Ceci était du à l'itération de calculs qui dégradent la précision (comme des cos/acos à répétition) qui fesaient diverger les valeurs.

Comment mesurer cette déviation? Comment garantir qu'un programme donné ne dépasse pas tel ou tel degré d'imprécision?
J'ai eu l'idée d'inclure une information de précision directement au niveau types numériques. Chaque entier et chaque flottant comporterait une information "précision" qui donnerais l'intervalle dans lequel se situe le nombre en question:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

type monFlottant = monFlottant { Float valeur; Int précision}

La précision d'un flottant étant 2^-23, monFlottant se trouve dans l'intervalle:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

monFlottant E [valeur - précision * 2^-23; valeur + précision * 2^-23]

(Evidemment, une arithmétique en virgule fixe serait plus appropriée!)

Il ne me reste plus qu'à définir tous les opérateurs traditionnels (+,-,*...) pour mes nouveaux types, chaque opération ayant un impact sur la valeur
mais aussi sur la précision.
Cela se résume à de l'algèbre sur les intervalles, ce qui est connu.
Par exemple, additionner un nombre à lui même double la taille de l'intervalle.

Grâce à ça, je suis capable de vérifier à l'éxécution que mon programme respecte certaines exigences de précision.
Ce qui me permet de détecter rapidement les algo abusifs à base de sin/asin!!! Fini les vaisseaux fantômes qui prennent les airs.


Embarquer la complexité

Existe-t-il un moyen de calculer automatiquement la complexité en O(...) d'un algorithme?
A priori, une analyse statique du programme devrait pouvoir le faire.
Je cite la documentation d'Haskell (deux fonctions prises "au hasard"):

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
size :: Map k a -> Int	Source
O(1). The number of elements in the map. 

member :: Ord k => k -> Map k a -> Bool	Source
O(log n). Is the key a member of the map?

Si un analyseur statique accède à cette information sur le O(...) de chaque fonction, il devrait pouvoir calculer la complexité d'un algorithme?
On pourrait ainsi s'assurer qu'on respecte des exigences de complexité sur l'ensemble d'un programme.

J'attend vos commentaires sur ces deux idées. Quelque chose existe dans ce sens?

[gorgonite]

Embarquer la précision

disons qu'il faut plutôt chercher à travailler sur des outils perdant le moins de précision possible... il n'y a qu'à voir la "tonne" d'astuces utilisables pour éviter ses erreurs d'arrondi sur les float

après, ajouter un calcul de précision en plus est potentiellement coûteux... et dépendra peut-être de la plate-forme et de bibliothèques tierces qui ne gèrent pas cette fonctionnalité

Si un analyseur statique accède à cette information sur le O(...) de chaque fonction, il devrait pouvoir calculer la complexité d'un algorithme?
On pourrait ainsi s'assurer qu'on respecte des exigences de complexité sur l'ensemble d'un programme.

on peut toujours "guider" l'analyseur, mais le principe de l'analyse globale est connu depuis des lustres... quid de la mise en oeuvre
on en avait fait une qui marchait plutôt bien, dans un cadre restreint... ça s'appelle les WCET

[Twinside]

Pour l'embarquement de la complexité, j'aimerais vraiment que les différents outil de génération de documentation prennent en compte une balise/tag @complexity ou un truc du style. Ca me semble tellement simple à mettre en place et pourrais rendre tellement service, et on peut même rêver à un outil qui résumerait les complexités des fonctions appelées à partir d'une fonction pour nous aider à calculer à la mano la complexité.

[Mac LAK]

Embarquer la précision

Le problème inhérent à ce calcul de précision, c'est que tu vas utiliser, justement, un outil qui n'a pas une précision supérieure.
Tout dépend de la précision globale dont tu as besoin, mais il te faut absolument être à une précision strictement inférieure à celle du processeur pour pouvoir "contrôler" la précision réelle attendue.

Ce qui implique, au plus simple, de travailler en virgule fixe et de calculer exclusivement via ce moyen, en contrôlant par des inégalités en précision maximale si tu es encore "dans les clous" ou non... Et de te refaire les fonctions mathématiques de base suivant ce système !!
Avec des langages orientés objet et supportant la surcharge d'opérateurs, l'implémentation sera "propre". Si par contre c'est en C, ça va en plus être très laid...

Si tu dois rester à la précision du processeur, il te faut alors absolument (au choix, peuvent être cumulés) :
- Restreindre la cumulation de calculs (ex : conserver les valeurs "d'origine" au lieu d'appliquer une fonction inverse),
- Utiliser des "floats" en public et des "double" en interne,
- Borner chaque résultat par une inégalité à une précision connue et fixée.

Dans tous les cas, cela va rajouter des calculs non négligeables à ton code, et cela peut avoir un impact important sur les performances.
D'expérience, le moins coûteux, c'est d'assurer une précision identique à celle d'un "float" (attention, c'est variable, la précision baisse si tu t'éloignes du zéro !), et de calculer systématiquement en "double".

Embarquer la complexité

A part via une preuve formelle, je ne vois pas trop comment le calculer automatiquement... Et ce n'est pas spécialement trivial.

Tu peux obtenir une complexité maximale théorique, mais le gros problème est de trouver le "n" dans le "O(n)" : quel sera le paramètre de la fonction le plus significatif ? Est-ce qu'un tel paramètre existe ? Si c'est le résultat d'une autre fonction, quid de la complexité de la fonction en question ?

Via une analyse statique du code et des boucles, j'ai bien peur qu'en cas de boucles un poil complexes, tu n'obtiennes pas de résultats probants (ex : obtenir O(n²) à la place de O(n.log(n))...). En tout cas, je n'ai pas de noms d'outils "tout prêts" permettant d'obtenir la complexité.



@Twinside : Tu peux toujours créer un alias sous Doxygen, par exemple... Il y a déjà les balises de pré/postcondition et d'invariant.

[LLB]

Tu peux analyser le code par métaprogrammation pour estimer la marge d'erreur. Il y a un exemple dans le livre Expert F# vers la page 250 : http://books.google.fr/books?id=NcrMkjVxahMC&pg=PA251

Ca peut te donner quelques idées.

[SpiceGuid]

Existe-t-il un moyen de calculer automatiquement la complexité en O(...) d'un algorithme?
A priori, une analyse statique du programme devrait pouvoir le faire.

C'est bien vrai qu'on manque d'outils de maîtrise/preuve de la complexité.
Quelques explications possibles qui me viennent à l'esprit :

1. la complexité n'a de sens que pour des fonctions totales
2. une analyse statique doit pouvoir le faire pour les cas simples, mais pour les autres je ne vois pas d'autre solution qu'une assistance de preuve (à supposer que ce soit possible). je ne sais pas démontrer que la division rapide a la même complexité que la multiplication Karatsuba (3 fois plus d'appels récursifs pour 2 fois plus de données) et je ne m'attends pas à ce qu'un analyseur über-cool le fasse à ma place
3. il y a plusieurs jugements de complexité (pire des cas,meilleur des cas,moyenne,amortie) et heureusement parfois la complexité pour des données typiques n'a rien à voir avec le pire des cas
4. il y a un problème de passage à l'échelle, "complexité sur l'ensemble d'un programme" ça n'a de signification que pour des programmes jouets fortements algorithmiques. dans une application ce qui est recherché c'est borner un temps de réaction, c'est en général bien plus difficile, on ne juge plus un algo, on juge une implantation, éventuellement avec des capteurs, des communications, des boucles de rétro-action...

À mon avis parler de garanties en terme de complexité ça nous ramène au débat sur les types dépendants et l'intérêt (ou l'affliction monumentale) de remplacer toute l'intuition par de la logique.

[gorgonite]

[*]une analyse statique doit pouvoir le faire pour les cas simples, mais pour les autres je ne vois pas d'autre solution qu'une assistance de preuve

il y a des systèmes hybrides qui fonctionnent... j'ai vu un exemple de métrique sur Java qui permettait d'exprimer des ordres de grandeur sur la complexité

par ailleurs, je ne comprends vraiment pas en quoi l'analyse statique serait à la masse comparé à un assistant de preuve sur ce domaine... j'ai vu d'excellents résultats sur des cas de programmation "générique" avec peu d'effets de bords, et avec les modèles hiérarchiques émergents, il est rapide d'abstraire un bloc par sa complexité et de continuer l'analyse sans exploser la mémoire (papier en cours de soumission d'ailleurs )

[nikko34]

Lorsque je travaillais pour la marine, nous avions un simulateur maritime justement, dans lesquels les bateaux, au bout d'un certain temps... Volaient à quelques mètres au dessus de l'eau!!

Heureusement il existe des simulateurs bien programmés

[souviron34]

Embarquer la précision

Lorsque je travaillais pour la marine, nous avions un simulateur maritime justement, dans lesquels les bateaux, au bout d'un certain temps... Volaient à quelques mètres au dessus de l'eau!!
Ceci était du à l'itération de calculs qui dégradent la précision (comme des cos/acos à répétition) qui fesaient diverger les valeurs.
Embarquer la complexité

Avec ton exemple, je dirais que c'est plus une erreur de conception qu'une erreur de précision..

En effet, dans la conception même, il est avéré que les calculs ont une précision limitée.

Cependant il existe une contrainte : le bateau doit être sur l'eau..

Par conséquent, une mauvaise conception ne vérifiera pas l'altitude.

Une bonne vérifiera à chaque pas important (et corrigera si besoin est) de la variation due aux imprécisions de calculs.

Donc plutôt que de se lancer dans des choses "abracadabrantesques" pour tenter de pallier à un défaut de conception, il suffit de refaire une bonne conception..

La précision ne devrait intervenir (en paramètre) qu'en phases initiales et finales : on contraint à une précision de 1 cm, on vérifie que la précision est inférieure à cette limite à la fin. TOUS les calculs intermédiaires devraient être auto-vérificatifs...

Là on ne raisonne pas dans l'absolu, mais dans la réalité physique.... Il est donc physiquement impossible qu'un bateau soit en l'air. Tout calcul de l'altitude doit prende cette contrainte en compte....

Existe-t-il un moyen de calculer automatiquement la complexité en O(...) d'un algorithme?

Je laisse Gorgonite (spécialiste en ce domaine) te parler des preuves (à l'état de labos de recherche), mais dans la plupart des cas que j'ai vu, tu peux cerner relativement rapidement le noeud de la complexité.

Après, à savoir le terme exact en termes d'algorithmie, cela risque d'être délicat.. Surtout si tu souhaites le faire automatiquement.. Comme l'a souligné SpiceGuid, certains algos (un exemple simple : le Quick Sort) ont une complexité "moyenne" qui est très loin du pire cas, et d'autre part une complexité linéaire, suivant les jeux de données, peut être pire qu'une carrée si les données étaient arrangées différemment...

[Mindiell]

Avec ton exemple, je dirais que c'est plus une erreur de conception qu'une erreur de précision..
En effet, dans la conception même, il est avéré que les calculs ont une précision limitée.
Cependant il existe une contrainte : le bateau doit être sur l'eau..
Par conséquent, une mauvaise conception ne vérifiera pas l'altitude.
Une bonne vérifiera à chaque pas important (et corrigera si besoin est) de la variation due aux imprécisions de calculs.

Je ne fais que réagir à cette partie, mais si l'altitude des bateaux est prise en compte par rapport à la mer (vagues et creux, voire les sous-marins qui sont sous le niveau 0 la plupart du temps), un bateau ne cesse de monter et descendre, et on ne peut appliquer une contrainte telle que celle que tu cites je pense. A moins d'avoir la hauteur de la mer, mais à ce moment là, le bateau est dessus, point, il n'y aurait pas de calculs.

[el_slapper]

Je ne fais que réagir à cette partie, mais si l'altitude des bateaux est prise en compte par rapport à la mer (vagues et creux, voire les sous-marins qui sont sous le niveau 0 la plupart du temps), un bateau ne cesse de monter et descendre, et on ne peut appliquer une contrainte telle que celle que tu cites je pense. A moins d'avoir la hauteur de la mer, mais à ce moment là, le bateau est dessus, point, il n'y aurait pas de calculs.

Beeen, le truc, c'est que même si il y a déperdition de précision, l'altitude du bateau est un système stable. Par là, j'entends que si il est trop bas, la mer va le remonter(flottabilité) et si il est trop haut, la gravité va le faire redescendre. Le tout avec un amortissement, via les frottements, qui garantissent une stabilisation à la position d'équilibre.

Le calcul, donc, devrait comparer la flottabilité à une altitude données(et ça décroit très vite au fur et à mesure que l'on sort de l'eau) avec la gravité(plus ou moins constante). Et le bateau osciller autour de position réalistes(même si elles sont fausses, eu égard au manque de précision évoqué par ailleurs). Si il ne le fait pas, alors c'est bien un erreur de conception(ou alors on force l'altitude à zéro). Et si il le fait, c'est une erreur d'implémentation.

[kaukau]

Le coup du bateau n'était qu'un exemple (véridique), bien sur.
On peut en trouver des dixaines d'autres
L'objectif était d'illustrer le problème du contrôle de la précision des calculs dans un programme...
L'idéal serait de pouvoir prouver, d'une manière ou d'une autre (par exemple directement avec le système de types) que certaines données conservent une certaine précision au gré des calculs.
Si ce n'est pas le cas, on sort un warning, que ce soit à la compilation ou à l'éxécution, ou encore à l'aide d'un outils externe...