Re: Du haut niveau pour gérer correctement du bas niveau

Mais une question que j'avais posée est : qu'est-ce qui peut pousser un développeur à utiliser cette fonction en dehors des bornes 0 .. 63 ?

Là tu veux dire que tu trouves rare ce genre de situation ?

la majorité des codes l'utilisant se retrouveraient pénalisés d'un test inutile sur X86

Et là tu veux dire que finalement tu trouves fréquente ce genre de situation ? J'avoue que suis un peu perdu dans ce que tu me dis.

J'émettais bien l'hypothèse que les situation où on avait besoin de sortir de ces bornes étaient rares. En conséquence, la grande majorité de codes utilisant shift_right se retrouveraient pénalisés d'un test inutile sur X86 si les implémenteurs de langage haut niveau choisissaient tous ton approche, pour la simple est bonne raison qu'il ne sortiront jamais de ces bornes et que ce test dynamique s'avérait inutile pour eux. Certains langages, dont OCaml fait partie, semblent avoir fait le choix de ne garantir le bon comportement que sur l'intervalle O .. 63 pour des raisons tout à fait légitimes d'efficacité et de le documenter. Ainsi les cas exceptionnels qui ont besoin de sortir de ces bornes doivent coder leur propre fonction avec un test sur la valeur de l'entrée. C'est un choix qui me semblent tout à fait convenable d'un point de vue pragmatique. Tu dois bien reconnaître que ton projet est un cas bien particulier à but pédagogique que des programmeurs réaliseront peut dans la réalité. Rust va même jusqu'à refuser de compiler s'il détecte statiquement que l'on sort de ces bornes.

Une approche peut être plus mixte est celle de Haskell, qui se comprend et se tient aussi : mais tout cela reste une question de choix. Je suis allé voir le code qui nous intéresse et l'on trouve :

(W64# x#) `shift` (I# i#)
 | isTrue# (i# >=# 0#) = W64# (x# `shiftL#` i#)
 | otherwise = W64# (x# `shiftRL#` negateInt# i#)
(W64# x#) `shiftL` (I# i#) = W64# (x# `shiftL#` i#)
(W64# x#) `unsafeShiftL` (I# i#) = W64# (x# `uncheckedShiftL#` i#)
(W64# x#) `shiftR` (I# i#) = W64# (x# `shiftRL#` i#)
(W64# x#) `unsafeShiftR` (I# i#) = W64# (x# `uncheckedShiftRL#` i#)

Puis pour shiftL et shiftRl :

-- Wrappers for the shift operations. The uncheckedShift# family are
-- undefined when the amount being shifted by is greater than the size
-- in bits of Int#, so these wrappers perform a check and return
-- either zero or -1 appropriately.
--
-- Note that these wrappers still produce undefined results when the
-- second argument (the shift amount) is negative.
-- | Shift the argument left by the specified number of bits
-- (which must be non-negative).
shiftL# :: Word# -> Int# -> Word#
a `shiftL#` b | isTrue# (b >=# WORD_SIZE_IN_BITS#) = 0##
 | otherwise = a `uncheckedShiftL#` b
-- | Shift the argument right by the specified number of bits
-- (which must be non-negative).
-- The "RL" means "right, logical" (as opposed to RA for arithmetic)
-- (although an arithmetic right shift wouldn't make sense for Word#)
shiftRL# :: Word# -> Int# -> Word#
a `shiftRL#` b | isTrue# (b >=# WORD_SIZE_IN_BITS#) = 0##
 | otherwise = a `uncheckedShiftRL#` b

Ce qui revient peu ou prou à implémenter les fonctions << et >> comme je l'ai fait plus haut en OCaml à partir des versions fournies par la bibliothèque standard dans le module Int64. Les implémenteurs de la bibliothèque standard OCaml n'ont pas choisi cette approche, laissant le soin aux développeurs qui en ressentent le besoin de le faire eux même.

Cela étant il reste la question de la circularité du second argument, qui ne pose pas de problème en ADA, mais qui en pose un en Haskell :

>import Data.Word
>import Data.Bits
>(1 :: Word64) `shiftR` 64
0
>(1 :: Word64) `shiftR` (maxBound :: Int)
0
>(1 :: Word64) `shiftR` (maxBound :: Int) + 1
1

Raison pour laquelle j'avais posé la question qui, elle aussi, n'était pas dénuée de fondements. ;-)

Et puis bon, c'est quand même étrange de fournir, à haut niveau, un opérateur qui fournit le même quotient par 2^64 que par 1 dans un langage de haut niveau sous prétexte que certains processeurs ont ce comportement pour de simples raisons d'optimisation.

J'espère t'avoir fait comprendre que, bien que le comportement puissent apparaître étrange lorsqu'on l'ignore, ce n'était pas un choix dénué de fondements ni sans justifications tout à fait recevables. Le seul reproche que l'on peut faire à freePascal est de ne pas le documenter mais non d'avoir un tel comportement.

Sinon toujours en étant taquin, en poussant ton principe à l'extrême, je pourrais dire : un langage qui a besoin de tests unitaires n'est pas un langage haut niveau digne de ce nom. :-P

De tels langages existent et comme je ne suis pas sectaire je te propose la méthode B présentée au Collège de France par son concepteur.

Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

Présentation dont j'extrais deux diapos :

la RATP décide de supprimer les tests unitaires et d'intégration

Octobre 98 : lancement de la ligne 14

Depuis lors pas de problèmes avec le logiciel développé avec [soit 17 ans plus tard, et il tourne, tourne, tourne...]

pour remplacer l'ancienne méthodologie avec tests unitaires par celle-ci :

86.000 lignes en ADA ont été produites automatiquement

27.800 preuves ont été faites

92% ont été prouvés automatiquement par l'Atelier B

Coût des preuves interactives : 7 hommes-mois

Les preuves interactives sont moins chères que les tests

Tu vois ADA lui aussi n'est pas assez « haut niveau » finalement. En fait Ada est à la méthode B ce que OCaml est à Coq : le langage dans lequel est écrit son noyau ainsi que le langage cible vers lequel il « compile ». Coq qui a servi, par exemple, à ecrire un compilateur C certifié correct. Ce sont là des exemples de ce que peut faire la rigueur de la formalisation mathématique pour garantir l'absence de bug dans un logiciel, à condition d'être effectuée avec les outils et les langages adéquats. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.