Les logiques : notes en vrac

Cet autre exemple, c’est celui élémentaire d’une zone de mémoire allouée, dans laquelle on écrit et qu’on libère ensuite et dans laquelle on ne peut plus écrire quand elle a été libérée. La solution présentée un peu plus loin, est sûrement trop naïve pour être universelle, mais ce sera au moins un point de départ, en espérant qu’aucune erreur ou omission n’a été laissée.

Avant de voir comment il pourrait être possible de formuler ce cas, un retour sur la non‑pertinence de l’ordre des termes.

Peut‑être qu’il faudra finir par remettre ce principe en cause, mais pour le moment, l’ordre des termes est maintenu sans importance, ce qui peut surprendre quand il s’agit de formuler des séquences. C’est pourtant un mieux.

Quand dans un langage classique des opérations sont écrites, elles sont obligatoirement en séquence, la séquence est parfois quelconque, parfois importante, les deux cas ne sont pas distingués autrement que par des commentaires. Croire que l’ordre de certaines opérations est important quand il ne l’est pas, est autant un problème que de ne pas voir que l’ordre de certaines opérations est important.

En l’absence d’ordre imposé et donc arbitraire, les cas de relations d’ordre devant être vérifiées, doivent être tous formulés, ce qui rend les choses plus clair.

Par exemple dans « op1; op2; op3; op4 » on ne sait pas si l’ordre est important, si parfois un commentaire peut noter que op3 doit apparaître après op2, c’est le mieux qu’on puisse avoir et ça n’éclaire pas sur le reste, les commentaires omettant beaucoup de ce qui serait pertinent à noter. Pourquoi s’embêter avec, puisqu’ils ne sont pas vérifiés et difficilement maintenable, faut d’être vérifiables, justement.

Les termes d’une conjonction, ne représentent pas une séquence d’opérations et donc pas un programme. Un programme devrait toujours être représenter par un terme interprétable comme tel, dont les éléments sont dans un certain ordre, important ou pas, selon l’interprétation de ce terme. Mais les termes parlant de ce programme, ne sont pas dans le même cas. Leur ordre est sans importance, sauf mention contraire et quand la relation d’ordre entre deux opérations est importantes, les termes doivent le préciser, faute sinon de pouvoir vérifier ce qui doit l’être.

Les relations des exemples précédents, n’ont pas de direction, mais il est possible de formuler une direction avec des emplacement prévu dans les termes et des interprétation adéquates, mettant ces relation en rapport avec l’ordre des termes imbriqués dans le terme représentant le programme.

Par exemple, dans « (op1 a) & (op2 a) », la constante a peut être interprétée comme un lien entre les deux opérations, mais ce lien n’est pas orienté. Il peut être orienté avec une formulation comme par exemple « (op1 (before a)) & (op2 (after a)) ». Les relations impliquant des termes intermédiaires, pourrait être lues par une interprétation transitive.

C’est justement ce type de formulation qui pourrait être utile dans le cas qui doit être couvert, celui d’un bloc mémoire alloué, écrit, puis libéré, et dans lequel on ne peut plus écrire quand il est libéré.

En restant abstrait, il serait d’abord possible de poser qu’un bloc mémoire alloué doit être libéré, en posant que la vérification du terme correspondant à l’allocation, nécessite la vérification d’un terme correspondant à sa libération :

(alloc M S) : (free M). -- S est la taille à allouer.

On peut imaginer que (free M) peut être vérifié sans être entièrement déterminé. L’ordre des termes n’étant pas important, il serait possible de mentionner la libération avant de mentionner l’allocation, mais les deux termes devraient être en accord, comme avec toute résolution.

Vrai que la lecture d’une telle règle pourrait surprendre : comment une libération peut‑elle apparaître dans la définition d’une allocation ? Pour être plus à l’aise, il faudrait se familiariser avec l’idée que les règles ne sont pas des opérations, est que cette règle se lit ainsi : pour vérifier le terme représentant l’allocation de M, il faut que puisse aussi être vérifié un terme représentant la libération de M.

De même, un terme représentant l’écriture dans M, nécessiterait que soit vérifiable un terme représentant son allocation :

(write M V) : (alloc M (size V)).

Ce qui là encore, ne doit pas être compris comme signifiant qu’on alloue M quand on y écrit.

Un bout du programme pourrait être représenté par cette conjonction de termes vérifiés par les règles : 

(free M) & (write V) & (alloc M (size V)).

La conjonction est écrite dans n’importe quel ordre et ici, volontairement à l’envers pour le faire remarquer. Cette conjonction serait vérifiable si tous les termes sont en accord par leurs variables. Ça ne pose aucun problème, les règles et les conjonction n’étant pas des opérations, mais des règles et des propositions.

Pour que ces termes puissent représenter ceux d’un programme, il devrait incorporer une formulation de l’importance de l’ordre. Si on considère que les opérations ont toutes en commun d’avoir un terme (after X) et (before X), venant toujours au même endroit dans le terme, alors l’ordre des opérations, nécessaire au programme même s’il ne l’est à un modèle pur seulement représenté par des règles, pourrait être formulé ainsi :

((before @c) (alloc M S) : ((after @c) free M).

On peut déjà pressentir un problème : en pratique, on ne va pas libérer M juste après l’avoir alloué, la libération aura lieu après d’autres opération et on a un même @c dans les deux termes et alors free ne peut apparaître que juste après alloc. Il est possible d’y remédier ainsi :

(@t1 (alloc M S)) : (@T2 (free M)) & (order @t1 @T2).

Des explications sont nécessaires. L’exemple imagine qu’une opération est composée de deux termes. Le premier est l’identité de l’instance de l’opération, sans indication d’ordre cette fois, et le second terme est l’opération en elle‑même.

Même remarques pour l’opération free. Mais après le terme correspondant à cette opération, est ajouté un autre terme, signifiant que @T2 (une variable) doit suivre @t1 (une constante). On a toujours deux termes représentant une identité, car on désigne des instances connues, ici celle de l’opération alloc et de l’opération free. Mais cette fois, les deux identités ne sont pas les mêmes. L’interprétation de order est supposée transitive. Il faut noter que c’est la condition de alloc qui défini cet ordre, mais une condition de free pourrait en dire autant, même si les intentions ne sont pas les mêmes. Dans le cas de alloc, c’est une condition pour ne pas perdre de la mémoire, dans le cas de free, ce serait une condition de validité. Les deux devrait être en accord, dans le cas contraire, la définition des opérations n’est pas cohérente.

L’ordre dans lequel ces termes sont déterminés avant d’être vérifié, n’a toujours pas d’importance, on peut parler de la libération après ou avant de parler de l’allocation, mais un ordre entre les deux est bien défini, avec la différence cette fois que free n’est pas limité à suivre immédiatement alloc, d’autres opérations peuvent s’intercaler entre les deux.

On peut imaginer que les opérations d’écriture sont définies de la même manière, posant qu’un terme vérifiant l’allocation doit correspondre :

(@t2 (write M V)) : (@T1 (alloc M (size V)) & (order @T1 @t2).

On veut définir qu’il n’est pas possible d’écrire dans une zone mémoire libérée :

(@t2 (write M V)) : (@T1 (alloc M (size V)) & (order @T1 @t2) & not (@T (free M)).

C’est radical, mais contradictoire, le terme ajouté signifiant qu’il ne doit pas exister de libération de la zone de mémoire, ce qui n’est pas un problème pour l’écriture, mais empêche l’allocation, l’allocation posant qu’une libération doit être vérifiée. On pourrait poser que la libération doit avoir lieu après l’opération d’écriture, mais l’écriture n’est finalement pas concernée par la libération, seulement par l’allocation, qui lui est seule nécessaire. On peut même imaginer que certains M ne puisse être libéré. On peut imaginer que c’est plutôt la libération qui empêche toute écriture par la suite, ce qui serait plus justifié, en parlant de validité :

(@t2 (free M)) : (@T1 (alloc M S)) & (order @T1 @t2) & not (invalid-write M @t2).

(invalid-write M @T2) : (@T3 (write M V)) & (order (@T2 @T3).

Il est possible de même, de poser qu’aucune opération de libération du même bloc ne doit suivre.

La vérification (ou l’obligation de preuve, selon que la résolution automatique y parvient ou pas) qu’il n’y a pas d’opération d’écriture venant après la libération, est dans une règle séparée, pour une raison d’écriture : deux termes sont nécessaires pour l’exprimer, alors que la négation s’écrit pour un terme. C’est un choix qui a été fait, pas une nécessité formelle : on peut écrire « A & not B & C » mais on ne peut pas écrire«  A & not (B & C) », qui nécessite d’extraite la conjonction « B & C », d’en faire une règle « R : B & C. » et d’écrire « not R » au lieu de « not (B & C) ».

Dans ces exemples, il faut imaginer que M a sa propre identité aussi, sans quoi, ces règles n’ont pas de sens, comme elles s’appliqueraient à des M quelconques. Cette identité peut être celle de l’opération en question (deux constantes @c apparaissant dans une règle, sont les mêmes), mais pas nécessairement, toutefois en s’assurant que l’identité est pertinente.

Une chose à noter, est que même si aucun exemple en faisant autant usage n’avait encore été donné, les exemples précédents font usage de notions de relation qui ne sont pas nouvelles, elles ont toujours existé dans le langage défini. Mais ces relations n’auraient pas le sens qu’elles peuvent avoir sans cette chose simple et pourtant tellement utile, que sont ces constantes représentant une identité, automatiquement instanciées. C’est autant utile que l’introduction des hypothèses, mais plus simple à la fois.

C’est verbeux, mais simple et remplit son rôle et ça semble correcte. Il pourrait être remédié aux côté verbeux par des idiomes pris en charge par une syntaxe au dessus de celle du langage. Cette syntaxe et les termes qu’elles produirait en la traduisant, pourrait être définis dans le langage lui‑même.

La formulation peut même être rendu plus générale de deux manières. Plutôt qu’un invalid-write, il est possible d’avoir un schéma de règle correspondant à « invalid Op » où Op pourrait être write ou autre chose. Cette ré‑écriture permettrait de mentionner les opérations invalides en général. Plutôt que dire qu’il ne doit exister aucune opération d’écriture après la libération de M, il serait possible de dire qu’il ne doit exister aucune opération sur M après sa libération, ce qui inclurait automatiquement une écriture ou une seconde libération.


Un exemple pour être plus clair.

Si M n’a pas d’identité, alors deux allocations équivalentes ne pourraient pas être distinguées et la libération s’appliquerait sur n’importe laquelle de ces allocations équivalentes d’un certain point de vue, comme la taille :

(@t1 (alloc M 2)) & (@t2 (alloc M 2)) & (@t3 (free M)).

On a deux termes correspondant à une allocation (instances d’opérations différentes, car avec une identité différente) et un seul terme correspondant à une libération, avec le même M dans les trois termes. Si M n’a pas d’identité, cette formulation est possible (elle est en accord avec les règles du message précédent), mais devient impossible si M a une identité. Alors dans ce cas, les deux premiers termes de la conjonction se contredisent.

Implicitement, les M sont des termes composés ayant leur propre identité, il ne suffit pas qu’ils aient la même taille pour être les mêmes. Les exemples du message précédents, abstraits pour être lisibles, l’omettent dans l’écriture.

L’idée de constantes représentant des identités abstraites, automatiquement instanciées, est peut‑être simple, mais représente une rupture qu’il faut exposer, sans encore savoir si ce n’est qu’une solution ad‑hoc ou si c’est un concept fondamental incontournable.

Jusque maintenant, tous les termes étaient des constructions, dont les propriétés étaient vérifiées par lecture et mise en correspondance, ces deux interprétations étant essentiellement réalisées par l’unification.

Ces constantes représentant une identité, ont nécessairement une représentation interne dans une mise en œuvre du langage, mais, au contraire des termes habituels, sont abstraites et opaques pour une application du langage, pour laquelle elles sont comme une sorte de magie ou une chose qui est là parce qu’elle est là.

Pour reprendre les exemples précédents, représenter la position d’une opération dans une séquence d’opération, par une identité abstraite, empêche une mise en correspondance directe entre cette position dans un terme concret et sa représentation abstraite. Concrètement pour être plus compréhensible, si dans une séquence d’opérations représentée par un terme, une opération Op1 apparaît comme le quatrième terme de la séquence et qu’une opération Op2 apparaît comme le sixième terme de la séquence, que ces opérations sont décrites ailleurs, chacune avec une position représentée par une identité abstraite, disons @t1 et @t2, alors pour vérifier que (order @t1 @t2) correspond bien à l’ordre de 4 et 6, il faut vérifier une équivalence entre les positions abstraites et les indexes ou vérifier une équivalence entre la relation d’ordre sur les positions abstraites et la relation d’ordre sur les indexes dans le terme représentant concrètement la séquence d’opérations.

Cette équivalence n’est pas nécessaire quand on a l’égalité. Mais on ne peut pas avoir d’égalité entre un terme concret comme un indexe, et un terme abstrait. Une preuve de l’équivalence nécessiterait une preuve de l’unicité des indexes, au minimum. Intuitivement, c’est trivial, mais peut‑être que en pratique ça ne l’est pas autant.

Il a été dit qu’une identité est une solution unique et qu’une solution unique est une identité. Chaque indexe est un terme unique bien défini, ce qui peut faire se demander s’il est vraiment nécessaire d’utiliser des identités abstraites, quand il n’est pas impossible d’avoir des identités concrètes.

Mais ce n’est peut‑être pas si simple. En dehors du fait qu’on peut imaginer qu’il soit plus commode pour modéliser, de pouvoir faire usage d’identités abstraites plutôt que de définir des objets concrets arbitraires ayant les mêmes propriétés, il n’est pas garanti que dans le monde réel ou les choses concrètes (même sous forme écrite), les identité puissent toujours être représentées par un terme exacte garantissant leur identité.

Un exemple permettra de mieux le comprendre. Imaginons que les entrées d’un programme soient des événements reçus en séquence. Ces événements peuvent être littéralement identiques, tout en se distinguant malgré tout par l’instant auquel ils sont reçus. Ils seraient distingués par une identité qui serait une position dans le temps. Cette identité pourrait avoir une représentation concrète, qui serait un horodatage … ou pas. Ou pas, parce qu’un horodatage a une granularité. Si l’horodatage est précis à la seconde près, deux événements reçus dans la même seconde seront associés à la même position dans le temps, alors que l’un a été reçu avant l’autre. On pourrait imaginer utiliser un horodatage plus précis. Mais ça ne résoudrait pas le problème, parce qu’il aura toujours une granularité et la possibilité que deux événements se suivant soient associés à la même position dans le temps alors que l’un suit l’autre, ne sera pas évitée.

On pourrait penser à utiliser un compteur associant des numéros uniques et successifs à chaque événement, plutôt que les situer dans le temps, les numéros ayant la même relation d’ordre que celle de l’arrivé des événements. Ce serait en fait une autre forme d’identité automatiquement produite, ne représentant plus la position concrète, une position dans le temps, mais seulement leur ordre d’arrivé, ce qui n’est pas la même chose. En effet, il pourrait s’écouler 20 minutes entre les événements #1 et #2 et à peine une seconde entre les événements #2 et #3, ce qui illustre que la notion d’ordre est préservée, mais plus la notion de temps tel qu’on le comprends et on a alors finalement là aussi, une abstraction se substitue à la place de la représentation d’une chose concrète.

L’appréciation à faire de cette identité, n’a peut‑être pas de réponse unique. Dans le cas précédent, il n’existe apparemment pas d’autre solution, les autres solutions étant une substitution d’une abstraction par une autre abstraction. Dans d’autres cas, cette identité est peut‑être seulement une commodité pour modéliser, mais qui deviendrait un obstacle à franchir pour passer du modèle à une chose concrète. Ce cas est celui où on substitue une chose ayant une identité intrinsèque, par une abstraction. Comme dit précédemment, une identité est une solution unique et une solution unique est une identité. Cette remarque est justifiée, la question d’origine ayant été celle que des choses ne peuvent qu’avoir une solution unique et de pouvoir le poser, le représenter, l’avoir comme terme. Seulement, il est plus difficile de traiter avec l’idée d’une solution unique en général, qu’avec une identité abstraite et opaque, instanciée automatiquement. Prouver qu’un terme a une solution unique, est un attente qui a fait son apparition assez tôt, mais qui n’a pas de solution générale pour le moment, contrairement à l’identité abstraite dont il est question ici.

Pour résumer en moins de mots encore : l’identité abstraite semble la solution pour certaines choses, jusqu’à preuve du contraire au moins, et est une commodité épargnant de résoudre un problème qui n’a pas de solution simple et générale, dans d’autres cas, des autres cas avec lesquels prouver qu’on utilise comme identité, des termes concrets ayant exactement au moins une et au plus une seule solution, serait la solution idéale, mais elle n’est pas évidente et cette solution n’existe pas encore.

La reprise à partir de ce point de départ, pour couvrir plus que ce qui a été couvert et qui ne répondait pas à tous les besoins pratiques, est moins facile à suivre. Une histoire qui pourrait s’appeler “ Lost in relations ”, mais qui fini bien.

On a jusque là défini pour un bloc de mémoire, l’allocation, l’écriture et la libération, avec des conditions de relations d’ordre entre ces opérations, des conditions qui leur donne leur signification et leur pertinence.

Même si ce n’est pas une condition de validité technique, il y a aussi un effet de l’ordre des opération d’écriture : une écriture efface la précédente. Entre la condition de validité technique de l’opération et le simple effet idempotent pas trop important, il y a la condition de validité sémantique, si on introduit la lecture. L’opération de lecture n’a pas été abordée. On ne peut pas lire avant d’avoir écrit, et ce qu’on lit dépend ce qui a été écrit précédemment.

C’est un classique, mais à rappeler pour poser le contexte. Si X est écrit dans M, puis que le contenu de M est lu, X sera retrouvé. Si une seconde écriture est faite dans M, avec Y, puis que le contenu de M est lu, cette fois c’est Y qui sera retrouvé. Deux erreurs courantes se présentent alors. La première, c’est quand le premier X est retrouvé comme une référence dans M, qui n’est donc plus X après la seconde écriture, mais est encore utilisé après comme si c’était X. La seconde, c’est quand il n’est pas connu qu’une seconde écriture a eu lieu, que X est sensé s’y trouver, que ce soit par référence ou pas, alors que c’est Y qui s’y trouve, pour avoir été écrit après X. Dans le premier cas, le résultat de la lecture change de valeur après la lecture, dans le second cas, le résultat de la lecture n’est pas celui attendu, suite à un changement de valeur avant la lecture.

C’est encore simplifié. La lecture de X par référence, peut se faire en ayant connaissance ou pas d’une possible écriture qui va changer sa valeur. Dans le premier cas, c’est équivalent à utiliser un M dont le contenu va changer sans opération d’écriture apparente. Une opération d’écriture doit pourtant bien avoir lieu, le contenu ne pouvant pas changer sans raison.

Les relations se compliquent, mais on peut imaginer qu’il serait possible d’associer une identité aux valeurs écrites (qui identifierait des significations et non‑pas des positions relatives dans le temps) et de poser des conditions de validité pour s’assurer du sens de ce qu’on lit dans M ou utilise provenant de M. Désigner M n’est alors plus suffisant, pour lire son contenu, il faut désigner M et l’identité de ce qu’on attend d’y retrouver.

Imaginons que dans M soit d’abord écrit le résultat du calcul d’un périmètre, puis ensuite, le résultat du calcul d’une surface. On va associer une identité au résultat du calcul du périmètre et de même pour la valeur de la surface. Cet identité n’est pas la valeur qui n’est pas connue à priori, comme elle est probablement variable, cette identité représente la signification de la valeur ou son propos.

Une formulation possible, en faisant abstraction de certains détails pour alléger l’exemple et en utilisant pas exactement la même représentation que précédemment :

(write @tw M V @V) : ….

(read @tr M V @V) : … & (order @TW @tr) & not (overwritten @V M @TW @tr).

(overwritten @V M @TW @TR) : (write @TO M VO @VO) & (order @TW @TO) & (order @TO @TR) & not (eq @V @VO). -- Le dernier terme est discutable.

La première règle associe une identité @V à la valeur écrite V à l’instant @tw dans M. La seconde règle décrit la récupération de la valeur V ayant la signification @V dans M, à l’instant @tr. En plus d’autres conditions omises, cette règle doit vérifier que la lecture a lieu après l’écriture, et aussi que la valeur n’est pas sur‑écrite, c’est à dire pas modifiée, entre l’instant de l’écriture et l’instant de la lecture. La valeur est considérée comme sur‑écrite, s’il existe une opération d’écriture entre les instants @TW et @TR, d’une valeur qui n’a pas la signification dont l’identité est @V.

Même avec des omissions, c’est encore plus verbeux qu’avant, mais en s’y accrochant un peu, ça se comprend, et aussi c’est formulable.

Imaginons maintenant qu’on ne s’intéresse pas aux valeurs ou en tout cas à leur signification, mais à leur propriétés. Ben en fait, c’est la même chose. Par exemple on défini le calcul d’un périmètre comme « (perimeter V P1 P2 P3 …) » qui associe le périmètre de valeur V à la collection de points P1, P2, etc. Comment serait représentée une propriété de ce périmètre, une propriété comme par exemple « plus que zéro » ? Par un terme de la même nature, comme (greater V zero) ; il n’y a en effet pas de différence entre la manière de formuler une valeur et la manière de formuler une propriété de cette valeur, les deux s’écrivent avec des termes de la même nature. Mais plusieurs valeurs peuvent avoir une même propriété. Ce n’est pas un problème, on peut imaginer associer une même identité représentant une propriété, à plusieurs valeurs. Mais alors, on va probablement avoir besoin des deux identités selon l’usage et alors il faudrait alors écrire la valeur dans M une fois pour chaque propriété, en plus de une fois pour sa valeur. Mais la règle de la lecture le prendrait pour une sur‑écriture. Alors il faudrait associer dans M, non‑pas une, mais deux identités à la valeur écrite, une identité de sa signification et une identité de sa propriété.

Pour s’épargner de l’écrire, il suffit de l’imaginer intuitivement, surtout que ça va s’encombrer un peu plus loin. Si on raisonne sur un programme, on peut vouloir définir sur des valeurs, des propriétés qui n’ont pas été prévues par la description du programme lui‑même, et il faudrait alors modifier ses règles pour le besoin des choses qu’on voudrait vérifier, puisqu’il faudrait prévoir dans certains termes du programme, une place pour les identités des propriétés nécessaires au raisonnement sur le programme.

Une solution pourrait être de séparer malgré tout, l’identité d’une valeur et l’identité d’une propriété, en catégorisant les identités elles‑mêmes, par une identité représentant leur catégorie. Il y a un petit piège volontaire : comme la phrase est formulée, dans le contexte de ce qui est dit, elle peut faire penser à quelque chose de la forme (@category @Id), mais si les catégorie sont fixées et connues d’avance, ce qui est le cas le plus probable, alors une constante ordinaire suffit, comme dans (category-1 @Id). Cette taquinerie qui ne veut pas faire tourner en bourrique, est pour aider à ne pas oublier qu’une constante représentant une identité, est d’abord une constante, seulement ensuite, ce qui la distingue des autres constantes, c’est qu’il en est instancié autant de fois qu’elle apparaît avec une instantiation de règle ou un nouveau contexte, ce qui est la même chose. Si les catégories sont connues d’avance et sont toutes valables dans le contexte global et donc aussi dans les contextes qui en dérivent, alors une constante ordinaire peut, et même doit, être utilisée. Doit, pour éviter les complications, pour une raison de validité d’usage qui sera exposée plus tard.

L’opération de lecture d’une valeur, préciserait qu’elle s’intéresse aux identités des valeurs et ne prendrait alors plus pour une sur‑écriture d’une valeur, l’établissement d’une propriété d’une valeur à un instant ultérieur à l’établissement de sa valeur. Elle le ferait en utilisant un terme comme (value @V) au lieu de @V tout‑court. Si le cas d’une propriété d’une valeur, ne venant qu’ultérieurement à l’écriture de cette valeur, semble seulement théorique, on peut imaginer un exemple pratique. Par exemple, l’utilisateur peut devoir entrer un nom qui est écrit quelque part, puis une vérification est faite pour savoir si ce nom est correctement écrit, toujours par le programme, donc à un instant ultérieur, le programme étant séquentiel, et alors il est légitime de positionner relativement dans le temps, la propriété, qui dans le temps vient après la valeur.

Il y aurait alors deux termes à écrire comme associés à l’identité d’une valeur, une écriture dans M pour la valeur et une écriture dans M pour la propriété. Il faut se souvenir encore ici, qu’un règle n’est pas une opération, mais décrit une opération. Parler d’écriture d’une propriété, ne signifie pas qu’ont décrit que le programme écrit une propriété en mémoire, ça signifie seulement qu’on se le représente ainsi, même s’il ne le fait pas réellement. C’est seulement quand on décrit que le programme écrit une valeur en mémoire, qu’il écrit une valeur en mémoire, et encore, seulement si on a posé cette interprétation d’une chose représentant un programme concret (par exemple un terme représentant un séquence d’opérations), parce qu’on peut parler d’un programme qui n’existe que dans une description, sans exister comme programme concret. Par exemple, on peut avoir écrit les règles de l’écriture et de la lecture, sans avoir défini de termes représentant les opérations correspondantes pour un programme réel dans un environnement défini. Par exemple encore, on peut décrire l’opération qu’est la somme de deux registres de 32 bits, sans avoir défini et associé une représentation binaire pour les instructions décrites.

Une propriété écrite étant typique rendue caduque par l’écriture d’une autre valeur au même endroit, la logique de l’écriture des propriétés (qui n’existe que dans la description) est la même que celle de l’écriture des valeurs. Surtout s’il existe plusieurs autres propriétés pouvant elle aussi être écrite, on peut vouloir une définition des opérations d’écriture et de lecture, qui dit que toute propriété écrite et correspondant à une valeur écrite, est rendue caduque par l’écriture d’une nouvelle valeur. Cette généralisation peut être obtenue avec des variables.

Remarque : si une propriété peut être dérivée d’un terme, il n’est pas nécessaire dans les exemples précédents, d’imaginer une écriture de la propriété associée à une valeur, la valeur suffisant à connaitre la propriété. Ce n’est pas toujours le cas. Un exemple du cas : une valeur est écrite en mémoire, c’est un nombre, on peut éventuellement déterminer que ce nombre est positif, parce que le programme ne produit jamais de nombre négatif, et alors il n’est pas nécessaire d’écrire cette propriété. Un exemple de cas contraire : une valeur est écrite, puis une autre ensuite, éventuellement littéralement la même, mais elles se distinguent par leur origine, par exemple en provenance d’un fichier pour la première, en provenance d’une connexion réseau pour la seconde. Cette propriété ne se dérive pas du terme seule, il faut l’associer explicitement à la valeur et comme la valeur est, dans la description, associée à une zone de mémoire, on associe cette propriété à la zone de mémoire dans laquelle se trouve cette valeur.

Pour résumer beaucoup ce message. Les constantes spéciales introduites permettent d’établir des relations entre des choses contextuellement ou en particulier au lieu de seulement en général. Il ne semble pour le moment au moins pas y avoir de limite théorique à ce qui peut‑être formulé avec ces relations, seulement une probable limite pratique, les relations nombreuses devant être formulées correctement pour correspondre à la sémantique du domaine d’interprétation (une zone de mémoire et ses opération d’allocation, écriture, lecture et libération, dans les messages précédents), ce qui est plus facile avec des cas simples qu’avec des cas complexes. Les constantes spéciales sont avant tout des constantes, si leur porté est prévue pour être globale, il est probablement préférable d’utiliser les constantes ordinaires, à définir en nombre fini dans le contexte global et initial.

Plusieurs remarques viendront plus tard, pour commenter des parties des derniers messages, incluant des parties de celui‑ci.

Avant les commentaires dont un important, une remarque sur les exemples choisis.

Les exemples ont été pris dans le domaine qui a été la raison initiale du langage défini, la vérification de propriétés de logiciel d’après une description logique. Comme les effets de bords des écritures et lectures impératives sont des sources de bug assez fréquents (pas les seuls, il y en a dans les programmes écrits dans un styles fonctionnels aussi), c’est cet exemple qui est venu immédiatement. Mais cet exemple ne parlerait pas à tout le monde, tandis que d’autres exemples parlant plus à tout le monde, pourraient être pris tout en étant parlant pour les gens concernés par les problèmes d’effets de bord, qui y verraient facilement une analogie d’un problème qui les concerne.

Plutôt que d’écriture dans un bloc de mémoire, il serait possible de prendre l’exemple du rangement dans un placard : on doit s’assurer qu’un casier est libre avant d’y ranger quelque chose, si on a rangé quelque chose à la place de ce qu’on y avait mis, ce qu’on y retrouvera est la chose qu’on y a mis en deuxième, pas celle qu’on y a mis en premier et y retrouve pas ce qu’on pensait y trouver si on l’a oublié. Un exemple de propriété pouvant être associé à ce qui rangé dans un casier, est par exemple de savoir si ce qui s’y trouve est à soi ou si on nous l’a confié, un attribut dont dépend la possibilité de disposer comme on veut ou pas, du contenu de ce casier, indépendamment de ce qui s’y trouve concrètement.

En plus d’être plus parlant pour tout le monde, tout en étant compréhensible pour les gens concernés par les effets de bord, ce type d’exemple aurait aussi plus d’intérêt sémantique en général, concernant par exemple des choses qu’on appel le‑bon‑sens, qui sont un exemple d’implicite dans la sémantique des langues naturelles.

Le commentaire important, précédemment annoncé.

L’idée des constantes spéciales instanciées, nécessite de définir un nouveau processus d’instanciation pour les règle qui les produisent. L’instanciation de ces règles est en bonne partie la même que jusque maintenant, avec une différence qui ne s’applique qu’à ces règles : elles sont à conserver dans le contexte. Mais en fait, non, elles ne sont pas différentes des autres, ce n’est qu’une illusion, les règles vues jusque maintenant étaient aussi dans le même cas, juste sans le faire remarquer … à un délicat détail près.

Explications …

Deux choses dites sont à remettre en question. Voici les deux premières citations concernées (une troisième est à revoir, elle sera rapportée plus loin) :





Finalement si, même l’idée des constantes instanciées avec les règles, impliquent une création de règles, même si le cas est différent de celui qui était redouté car douteux. La différence principale, est que les règles ajoutées ne sont pas cachées, elles sont définies globalement sous une forme abstraite, puis ajoutées aux contextes sous des formes spécialisées ou déterminées.

On peut voir une similitude entre une règle comme « (r @c). » et une règle comme « (s c). » La seconde est vérifiable par le terme (s c) ou le terme (s V), si V est libre ou liée à c. Quand elle est posée, la règle « (s c). » pose un fait.

Par quoi est vérifiable la règle « (r @c). » ? Elle est vérifiable par le terme « (r V) » si V est libre et V est alors liée à une constante unique générée en lieu et place de @c. Mais il n’y a pas d’équivalent du cas plus haut, celui de la vérification par un terme constant. La règle « (r @c). » n’est vérifiable que par un terme dont le second argument (si on peut dire) est la constant instanciée par @c. Elle n’est pas vérifiable par (r @c), car bien que le texte des deux termes soient les mêmes, les deux constantes sont obligatoirement différentes, puisqu’elles représentent deux créations de constantes, chaque constante créée étant unique. Donc pour le moment, on a seulement que cette règle est vérifiable si l’argument est une variable libre, qui sera alors liée à la constante produite. On ne peut, semble‑t‑il, la vérifier avec une constante que indirectement, par une variable liée à la constante instanciée avec la règle. Mais ça n’est pas possible non‑plus, car même en ayant instancié « (r @c). »  puis capturé la constante produite dans une variable d’une manière quelconque, la vérification de (r V) créera une nouvelle constante en instanciant une seconde fois la règle « (r @c). » et la constante capturée dans la variable et celle de la nouvelle instance de « (r @c). », ne correspondront pas.

Les exemples de ce qui peut être exprimé avec ces constantes, étaient autant sensés que incontournablement utiles, mais il semble autant aussi que le processus de vérification des règles impliquant ces constantes, soit une impossibilité.

Si c’était vraiment impossible, les mots employés n’auraient pas caché le désappointement, immédiatement. En fait, la vérification de « (r @c). » ne doit pas que instancier la constante unique correspondant à @c, elle doit instancier aussi la règle, mais pas dans la même sens que les autres règles, plus dans le sens des variables et de ces constantes, c’est à dire en conservant l’instance de la règle dans le contexte. Il faut reprendre. Disons qu’on veuille vérifier le terme (r V). On instancie la règle « (r @c). », une constante est produite, disons c_1, même si elle est abstraite et opaque, parce que sans représenter sa valeur, ce serait incompréhensible. La variable V va être liée à cette constante c_1, mais en plus aussi, la règle « (r c_1). » va être ajoutée dans le contexte. Que ce passe‑t‑il alors quand on veut à nouveaux vérifier le terme (r V) ? La variable V a été liée à c_1, on se retrouve donc dans la même situation que si on voulait vérifier (r c_1), hors, c’est justement la règle qui a été ajoutée dans le contexte. On a déjà une similitude avec une précédente idée d’hypothèses déposées dans le contexte.

Pour résumer jusque là : la création d’une de ces constantes, nécessite la création d’une nouvelle règle, associé à la création de la constante. Cette règle ajoutée, c’est la règle qui a produit la constante. La règle sous sa forme non‑instanciée, sa forme telle‑quelle, est comme un schéma abstrait, avec des paries variables spéciales, qui ne peuvent être mise en correspondance qu’avec une variable libre et rien d’autre. Ensuite, ce qui peut être vérifié avec une possibilité supplémentaire, c’est la règle produite avec la constante, ou plutôt encore, pour la constante, parce que sans l’ajout de cette règle au contexte, la constante produite ne peut jamais correspondre à rien, excepté à une variable libre.

Ces règles semblent alors différentes des autres, mais en fait non, les autres étaient seulement un cas particulier, y compris les constantes ordinaires vues jusque maintenant : ces règles et ces constantes disponibles en permanence, sont comme instanciées et conservées dans le contexte globale. Mais comme le contexte globale est toujours le même, ça ne se remarquait pas, les règles n’étant pas recréés à chaque fois qu’on repartait à partir du contexte globale initial pour un système de règles posées.

Il a été fait mention de la disponibilité des règles, et c’est là que ça coince. Disons pour le moment que les règles ordinaire gardent quand‑même une différence avec ces nouvelles règles. C’est pour un peu plus loin.

Avant de continuer, parce qu’il reste à en dire, il faut revoir cette citation, qui elle aussi va devoir être comprise autrement qu’elle ne l’avait été :



Il y aurait un avantage à favoriser les variables spécialisées sur ces constantes, pas seulement pour la lisibilité, aussi un avantage technique. Ceci, ne pas permettre aux variables ordinaires non‑spécialisées d’être mise en correspondance avec ces constantes spéciales, serait sémantiquement douteux (car ne permettrait pas de vérifier ce qui a éventuellement du sens), alors il y a peu de chance qu’une telle limitation soit retenue. Il faut maintenant expliquer un problème laissé sans le mentionner et qui justifie ces interrogations.

L’instanciation de ces constantes nécessite donc que les règles dans lesquelles elles apparaissent littéralement (c’est à dire sous la forme @c et non‑pas sous le forme @V), soit conservées, parce que ces constantes spécialisent en fait des règles qui telles qu’elles, sont autant abstraites que les identités que représentent les constantes qu’elles portent.

Si on la règle « (r @c). » et que dans un corps de règle, on a un terme (r @V) ou même (r V), alors ce terme est‑il résoluble ? Ça dépend. Ça dépend de si la règle a été instanciée, c’est à dire de si on a par exemple une règle « (r c_1). » dans le contexte. Si cette instanciation a eu lieu avant que ne soit rencontré le terme (r @V), si @V est libre ou liée à c_1, alors le terme est vérifié. Mais si la règle n’a pas encore été instanciée et ne le sera qu’à l’occasion de la vérification d’un autre terme ? Alors dans ce cas, le terme (r @V) ne peut être dit, ni vérifiable, ni non‑vérifiable, parce qu’on ne peut pas le savoir à ce moment là.

C’est là que les règles ordinaires gardent une différence quand‑même, et importante : elles sont déjà toutes présentes, elles existent déjà toutes. Comment traiter avec des vérification de termes dont on ne sait pas si oui ou non, apparaîtra plus tard dans le contexte, une règle le vérifiant ? Comment savoir si oui ou non le terme n’est simplement pas vérifiable parce qu’aucune règle le vérifiant n’apparaîtra jamais ?

C’est une colle pour la résolution automatique et une suggestion que les preuves manuellement écrites sont parfois peut‑être la seule vérification possible. C’est aussi une suggestion que si on a pas prouvé qu’une chose est impossible, on ne peut supposer qu’elle l’est simplement parce qu’on a pas put prouver qu’elle est possible. Le problème qui se pose, dit à quel point il faut se méfier d’une telle supposition.

C’est d’autant plus délicat à aborder, que l’apparition d’une règle nécessaire à la vérification d’un terme, peut elle même dépendre de la vérification d’un terme. C’est délicat aussi dans le sens où ça rend difficile la préservation de la non‑importance de l’ordre des termes. Mais cette non‑importance, sera préservée, même si la solution pour y parvenir est difficile, car l’importance de l’ordre des termes, signifierait que le sens de ce qui est écrit n’est peut‑être pas celui qu’on croit, ça équivaudrait à dire qu’il faudrait parler de débogage pour des descriptions, ce qui n’est pas acceptable. Vérifier des propriétés dérivées d’une description pour vérifier sa pertinence ou se rassurer sur sa bonne signification, oui, mais que l’ordre des termes ait une importance, ce n’est pas le même problème, c’est trop de risque. Je crois personnellement que la non‑importance de l’ordre des terme peut toujours être préservée, quand les termes ont une sémantique déterministe, ce qui est le cas jusqu’ici au moins.

Une solution serait peut‑être de faire une vérification en plusieurs passages. Les termes non‑vérifiés pour cause de contradiction avec le contexte, seraient considérés comme non‑vérifiés avec certitude. Les termes non‑vérifiés faute de tête de règle candidate, seraient considérés comme dans un état incertain. Si une règle échoue parce qu’un de ces termes est en échec certain, alors la règle est en échec certain, en échec incertain dans le cas contraire. Les status des échecs seraient ainsi remontés. Le processus de résolution ou de vérification se déroulerait ainsi presque comme il a toujours été fait, à cette seule différence des termes en situation incertaine. Puis quand la recherche de solution (sous réserve qu’elle ne tombe pas dans une récursion infinie) a épuisé toute les solutions à tenter, alors elle reprend depuis le début et de la même manière, mais en ayant conservé dans le contexte, les règles spéciales et les constantes associées, qui auront été déposées pendant cette itération et les itérations précédentes. Si au cours d’une itération, aucune modification n’a été apporté aux contextes, alors il est considéré qu’ils sont fixés, que les échecs y sont tous des échecs définitifs. La difficulté serait de réitérer une recherche de solutions, en revenant correctement dans les contextes conservés des précédentes itérations. Il faudrait ne pas récréer des contextes qui ont déjà été créés et au lieu de les créer, d’y revenir pour éventuellement les compléter, mais en même temps, distinguer les contextes réellement nouveau, dans lesquels il n’avait pas put être entré lors de l’itération précédente et qu’il faut créer.

C’est une brique sur la tête, mais au moins, elle laisse les idées claires, même si elle assomme, mais tout est clair quand‑même.

L’avantage des variables spécialisées, c’est à dire de préférer @V à V, n’a pas été décrit. Ce qui suit est en oubliant pas qu’il est malgré tout prévu de ne pas poser cette restriction.

Quand devant un terme à vérifier (r @V), à moins que le terme ne soit en contradiction avec le contexte, si on ne parvient pas à le vérifier, faute de savoir si c’est seulement parce que la règle nécessaire n’est pas encore présente dans le contexte, on a au moins une forte raison de se poser la question, comme @V, variable spécialisée, ne peut que correspondre à une constante produite par une constante abstraite. Si le terme est (r V), on se pose peut‑être la question en vain. S’il y avait un avantage à préférer @V à V, il serait là, dans le fait que @V serait une indication.

Une chose omise dans le message précédent. En plus de ne pas savoir si un terme (r @V) n’est pas vérifiable parce que la règle correspondante n’a pas été créé, si @V est libre, il est aussi possible de se demander s’il faut tenter de vérifier le terme en instanciant la règle abstraite correspondante ou s’il faut attendre que @V soit liée ailleurs pour ensuite vérifier le terme avec une instance de la règle au lieu d’en instancier une nouvelle. Dit en moins de mots, avec @V libre, on ne sait pas à priori s’il faut tenter de la lier à une nouvelle instance d’une constante abstraite ou tenter de la lier à une instance déjà existante ou qui viendra plus tard. Il y a là un risque de recherche qui ne se termine jamais, en agrandissant l’espace de recherche pendant le cours de la recherche d’une solution, comme la source des nouvelles instances d’une constante et d’une règle abstraite (les deux instances viennent toujours ensemble), est théoriquement inépuisable ou seulement arrêtée par les limites de la mémoire disponible. Il faut bien tenter d’instancier une règle abstraite, sinon elles ne sont jamais instanciées, mais en instancier une chaque fois que l’occasion se présente, faite courir à la fois le risque de produire un grand nombre échecs par contradiction et à la fois le risque d’augmenter rapidement et inutilement, le nombre d’instances de règles candidates. Savoir quand instancier et quand ne pas instancier, et peut‑être le problème le plus difficile à solutionner.

Dans certains messages précédents, quand il a été question de l’identité d’une valeur, il ne faut pas comprendre que l’identité est associée à une valeur au sens d’un terme entièrement déterminé, mais à une valeur qui est un terme pas nécessairement déterminé. Il faut le comprendre comme l’identité du sens de la valeur ou du sens du terme qu’on tient pour une valeur.

Il faut le préciser, comme il a été dit aussi avant, qu’une solution unique est une identité et qu’une identité est une solution unique, ce qui peut prêter à confusion. C’est plutôt le cas de certaines identités.

On peut représenter une solution unique par une identité abstraite, de même qu’on peut utiliser une identité abstraite pour représenter une solution à une chose bien déterminée, mais dont la valeur n’est pas déterminée, appartient seulement à un ensemble, est variable.

Le vocabulaire serait à revoir, il n’est pas clair.

Il semble maintenant nécessaire d’introduire un nouveau type de terme : des termes sous forme de conjonction, à ne pas confondre avec les conjonctions des règles.


Savoir quand instancier … La réponse faisait des coucous discrets dans les exemples donnés précédemment, dont voici une règle en extrait :

(@t1 (alloc M S)) : (@T2 (free M)) & (order @t1 @T2).

La réponse à la question est : surtout pas pendant une vérification de règle. Si dans l’exemple de cette règle, on instanciait une règle abstraite correspondant à (@T2 (free M)) pendant qu’est vérifiée la règle abstraite (@t1 (alloc M S)), alors les règles ne vérifieraient plus ce qui est posé, elles poseraient elles mêmes ce qu’elles sont sensées seulement vérifier. En moins de mots : les règles ne vérifieraient plus des faits, elles n’auraient donc plus de sens.

La réponse à cette question de savoir quand instancier pendant une vérification de règle est donc : jamais. Ce qui fait revenir l’autre question déjà posée : il faut pourtant bien pouvoir instancier ces termes, mais alors quand ?

La réponse est probablement : quand on pose des faits. Là encore, les exemples venus spontanément le disaient sans bruit :

Cet exemple était écrit comme une conjonction, ce qui allait de soi, mais les seules conjonctions vues jusque maintenant apparaissaient dans des corps de règles et cette conjonction là, n’est pas un corps de règle, elle est un fait posé, un fait représenté par une conjonction de termes. C’est quand ce fait est posé, que les règles abstraites sont instanciées pour devenir des faits concrets, dont il devra être vérifié qu’ils vérifient bien les conditions définies par la règle à laquelle ils correspondent. Les instances sont alors connues avant la vérification des règles, on a plus à se demander s’il en viendra une plus tard ou pas pendant la vérification.

Les faits avaient été jusque maintenant des règles. Un fait posé littéralement, était jusque maintenant, une règle dont le corps est vide. Mais on ne peut pas donner le même status à une règle comme «(nat z). » et à une conjonction de termes comme plus haut, non ? Les deux sont pourtant des faits posés et inconditionnels. La seule différence entre les deux, serait que la règle «(nat z). » est nécessaire pour que les autres règles de nat soit au moins satisfiables. Disons que «(nat z). » serait un fait fondamentale, tandis que la conjonction plus haut, est un fait d’une application du langage. Il y a quand‑même une différence : «(nat z). » n’a pas à être vérifié comme un terme (elle doit seulement être vérifiée satisfiable), tandis que la conjonction de termes plus haut, est sensée l’être.

Implicitement, jusque maintenant il avait été imaginé qu’un programme par exemple, serait décrit par un gros terme ordinaire, juste beaucoup plus gros que les exemples de termes vus jusqu’ici, et que ce terme serait passé en argument à une vérification de règle. Il semble maintenant qu’il serait plutôt décrit par une discours ayant un status à part des termes. Ce discours serait une collection de faits, à ne pas confondre avec les faits posés comme des règles inconditionnelles. Mais comment alors faire une vérification sur ce discours ? Déjà des vérifications à partir des faits qu’il pose et peut‑être aussi en permettant de désigner certains ensemble de fait, comme par exemple :

procedure-1 : (free M) & (write V) & (alloc M (size V)).
procedure-2 : …
etc.

Chacun des termes composant les conjonctions, serait un fait unique (c’est là que les identités abstraites peuvent être parfois nécessaires), intriqué ou pas aux autres faits de la conjonction dans laquelle il apparaît. Il pourrait aussi être possible de se placer dans le contexte des faits posés par “ procedure-1 ” en particulier. Ce n’est qu’une vague idée, il est prévisible que des remarques seront encore à faire. Par exemple, il faudrait préciser comment procedure-1 pourrait être interprété comme un terme ordinaire, sur lequel il serait tenté de vérifier des règles.

Avant des commentaires à la suite du message précédent, une révision du vocabulaires.

Parler de constantes spéciales à tout bout de champs, c’est vague. Chaque fois qu’une chose est nouvellement introduite, elle est appelée spéciale, c’est abusé. Ce ne sont pas des constantes spéciales, ce sont des identités abstraites. Pas des identités tout‑court, parce qu’une identité n’est pas toujours abstraite. En fait, les trois types de constantes connues dans le langage jusqu’ici, une explicite, une implicite et une entre les deux, sont toutes les trois des identités abstraites. Il faut quand‑même les distinguer, mais sans oublier ce qu’elles sont en commun. Les premières constantes apparues, explicites, plusieurs fois vaguement appelées les constantes ordinaires, sont des symboles (des symboles arbitraires mais déterminés). Les secondes apparues, implicites, sont les variables apparaissant dans des hypothèses, elles pourraient être appelées des constantes abstraites de substitution, comme elle se substitue à un terme variable. Les troisièmes apparues, entre les deux, parce que à la fois implicites et explicites, se déclinent en deux cas. Ce qui a été noté @c, pourrait être appelé une instance d’identité, mais comme il n’est encore pas tout à fait certain qu’elles sont nécessaires, alors c’est sous réserve.