Embarquer plus d'informations dans le code: la précision et la complexité
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:
type monFlottant = monFlottant { Float valeur; Int précision}
La précision d'un flottant étant 2^-23, monFlottant se trouve dans l'intervalle:
Code:
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:
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?
