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

Afr, mon compilateur interne vient d'émettre un warning : risque de boucle sans fin, abort envisageable au prochain tour. ;-)

C'est ce que j'expliquais dans un ancien post.

Je le sais bien c'est le premier commentaire de ce sous-fil : on boucle !!! Qu'est-ce que tu n'as pas compris dans ma réponse ? Tu m'as pourtant répondu que j'avais était très clair, là c'est moi qui ne te comprends plus.

Si OCaml disposait de la notion de sous types (contraints) alors il disposerait de deux fonctions shr.

J'espère que tu me pardonneras la familiarité de l'expression mais j'ai envie de te répondre : « si ma tante en avait, on l'appellerait mon oncle ». J'avais pourtant précisé dans ma réponse que les systèmes de typage était une question distincte, bien qu'elle puisse être utilisée dans le cas de Ada pour traiter le problème. Mais jusqu'à preuve du contraire, un langage doit faire avec le système de type dont il dispose. À ma connaissance il n'y a aucun plan pour intégrer cette sorte de type dans le langage, ce que je peux comprendre pour des raisons théoriques liées aux fondements du langage qu'ils seraient trop longs de développer (il y a néanmoins des sous-types contraints en OCaml, mais pas de la sorte des types range comme en Ada).

Connais tu la théorie des types ? J'avais pourtant donner un lien vers un dossier de la gazette des mathématiciens sur le sujet, l'as-tu lu ? Outre son utilité pour le typage statique des langages fonctionnelles, le système F (qui est le fondement des système de type de Haskell et OCaml) a été inventé au début des années 70 par le mathématicien et logicien français Jean-Yves Girard pour des questions liées aux fondements des mathématiques. Je cite ici sa nécrologie à la page 14 :

En 1953, Takeuti remarquait que la logique du second ordre permettait de formuler sans axiomes toutes les mathématiques courantes, et il proposait un procédé effectif d’élimination des coupures pour étendre le théorème de Gentzen : c’est la conjecture de Takeuti. En 1965, Tait démontrait l’existence de démonstrations sans coupure pour le calcul des séquents de Takeuti, mais l’essentiel manquait, à savoir la convergence du procédé d’élimination proposé par Takeuti. C’est ce que j’ai démontré en 1970, dans l’article [1], résultat amélioré dans [2] et [3]. En fait, ce résultat se présentait comme un système de calcul fonctionnel typé, (le système F), dans lequel on pouvait définir un type nat des entiers (i.e. dont les objets sont les entiers), avec deux théorèmes principaux :

Théorème 1
Le procédé de calcul dans F converge (normalisation).

Théorème 2
Tout algorithme fonctionnel (envoyant les entiers dans les entiers) dont on peut établir la terminaison au moyen des mathématiques courantes, se représente dans F au moyen d’un objet de type nat ⇒ nat.

Le système F est par exemple utilisé par Haskell comme représentation intermédiaire pour son compilateur. Ce système a connu depuis différentes extensions, ou il y a eu d'autres système du même genre comme la théorie des types de Per Martin-Löf, le Calcul des Constructions (CoC) à la base de Coq qui devint le Calcul des Constructions Inductives, puis on a tout récemment la théorie homotopique des types. Ces théories tournent toutes autour d'une problématique : la recherche d'un système de formalisation unifié de l'ensemble de l'édifice mathématique, ainsi que la réponse à la question : « les mathématiques sont-elles cohérentes ? ». Parce que l'on parle d'arithmétique depuis le début, mais l'arithmétique est-elle une théorie cohérente ?

Pour revenir sur la question initiale du journal : le décalage bit à bit vers la droite. Dans un autre commentaire, tu as écris :

Haskel, Python, Ada, Eiffel le proposent. D'autres langages de haut niveau ne font rien de plus que le jeu d'instruction X86 et je trouve que c'est une faiblesse (générateur de bugs).

Premièrement ce que fait Haskell, la bibliothèque standard OCaml aurait pu tout aussi bien le faire : je l'ai expliqué précédemment; cela n'a pas été l'option retenue (j'ignore, néanmoins, les raisons qui ont déterminé un tel choix). Ce n'est pas lié au possibilité du langage mais à un choix d'implémentation pour la bibliothèque standard fournie avec le compilateur. Mais ce n'est pas la seule existante, elle a des concurrentes certains développeurs ne la jugeant pas assez fournie.

Deuxièmement mettre Python dans la liste sur des questions de sécurités de code : c'est une blague ou tu es sérieux ?

Troisièmement, vu que tu viens de rajouter une exigence à ton cahier des charges : ne pas avoir de types cycliques pour le paramètre déterminant le degré du décalage, tu viens de les perdre tous sauf Ada. La liste des langages qui trouve grâce à tes yeux s'amenuise de plus en plus au fur et à mesure que progresse la discussion. ;-)

Pour le cas de Haskell, je l'ai déjà illustré. Pour celui de Eiffel, si je lis la documentation

infix "|>>" (s: INTEGER_8): INTEGER_64
 Shift by s positions right (sign bit copied) bits falling off the end are lost.
bit_shift_right (s: INTEGER_8): INTEGER_64
 Shift by s positions right (sign bit copied) bits falling off the end are lost.

Déjà le paramètre est sur 8 bit, donc ton exercice n'est pas réalisable en Eiffel avec cette version de shift_right. Et si je lis la documentation sur les INTEGER_8, dans le résumé je vois : 8 bits signed integer. J'ai comme le pressentiment qu'il est cyclique lui aussi : si un développeur Eiffel pouvait confirmer mon intuition ?

Et pour le langage de départ du projet de tes élèves, FreePascal, outre le comportement du shr inattendu, il me semble bien d'après cette documentation que le type en question est lui aussi cyclique :

function isBitSet(AValue, ABitNumber:integer):boolean;
begin
 result:=odd(AValue shr ABitNumber);
end;

Ai-je raison de supposer que le type integer est cyclique en Pascal ?

Comme de tout le fil de discussion et de tous les commentaires je suis le seul à avoir pointé du doigt l'importance de la nature du type de ce paramètre, je suis au regret de devoir émettre une nouvelle hypothèse qui me chagrine en espérant me tromper. Le « bug » n'était pas anticipé et a été découvert par hasard, et malgré son apparente solution tu en es au même point d'incompréhension que tes élèves : la source fondamentale du problème c'est la différence de géométrie entre un tore et un cylindre. ;-)

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