Academic literature on the topic 'Logique de Hoare'

A közelmúltban az intelligens robotokban rejlő egyre növekvő
 veszélyek a mesterséges intelligenciáról (MI) szóló irodalom központi témájává váltak. Ez az általam „alarmistának” nevezett nézőpont logikus következménye (és erős szövetségese) az „erős MI” korosodó paradigmájának, illetve ezen paradigma legújabb változatainak. A veszélydiskurzus főbb argumentumainak és az ezekkel kapcsolatos problémák ismertetése után felvázolok egy új értelmezési keretet, melyben minden MI-rendszer elválaszthatatlan egységet, hibridet alkot humán komponensével,
 a funkcióval és környezetével. Véleményem szerint az igazán fontos kutatási, tervezési és fejlesztési kérdések a humán összetevővel, valamint a humán és a mesterséges komponens interakciójával kapcsolatosak. Ez a megközelítés három további diskurzus számára is teret nyit: az automatizáció következő szintje és a foglalkoztatás jövője, az emberi összetevő kiterjesztése és az ehhez kapcsolódó jogi és etikai kérdések, melyeket az MI és a robotika legújabb generációs fejlesztései vetnek fel.
 
 ---
 
 Artificial intelligence – why to redesign the discourses?
 
 The basic narrative of the 2014-2015 AI literature is the growing danger, incarnated by more intelligent robots. This position what I call „alarmist” is a logical consequence and powerful ally of the hoary „strong AI” paradigm and its brand-new versions and mutations. After reviewing current considerations against the alarmist approach, we provide an analytic framework to understand every AI-system as hybrid one, inseparable from its human component, function and environmental embeddedness. And what is more, we argue that the really important research, development and design issues are about the human component and its interaction with the artificial part. This perspective opens new horizons in three subdiscourse, too: the next level of automatization and the future of employment, the enhancement of the human part and the newborn legal and ethical issues, raised by the next generation improvements in AI and robotics.

En informatique comme dans de multiples autres domaines, les graphes peuvent être trouvés partout. Ils sont utilisés pour représenter des données dans des domaines allant de la chimie à l'architecture, en tant que structures abstraites ou que modèles des données et de leurs évolutions. Dans tous ces domaines, il est prévisible que les graphes évoluent au cours du temps suite à des réactions chimiques, une mise à jour des connaissance ou l'exécution d'un programme. Être capable de traiter ces transformations est une tâche particulièrement importante et difficile. Dans ce travail, notre objectif est d'étudier la vérification de telles transformations de graphes, c'est à dire comment prouver qu'une transformation de graphes est correcte. La correction d'une transformation est plus précisément définie comme la correction d'une spécification pour cette transformation contenant en plus une précondition et une postcondition. Nous avons décidé d'utiliser un calcul à la Hoare générant une plus faible précondition pour une postcondition et une transformation. Si cette plus faible précondition est impliquée par la précondition, la spécification est correcte. Nous avons choisi une approche plus algorithmique pour les transformation de graphes utilisant des actions atomiques. Nous définissons deux moyens de construire des transformations de graphes: en utilisant un langage impératif ou en utilisant des systèmes de règles de réécriture. Le principal ingrédient est la logique qui est choisie pour représenter la précondition, la postcondition et les possibles conditions internes. Pour que la logique puisse interagir avec le calcul, nous demandons que le problème de décision soit décidable, qu'elle soit fermée par substitutions et qu'elle soit capable d'exprimer l'existence ou l'absence d'un sous-graphe affecté par la transformation. Le résultat central de ce travail est l'identification et l'explication de ces conditions<br>In computer science as well as multiple other fields, graphs have become ubiquitous. They are used to represent data in domains ranging from chemistry to architecture, as abstract structures or as models of the data or its evolution. In all these domains, graphs are expected to evolve over time due to chemical reactions, update of the knowledge or programs. Being able to deal with such transformations is an extremely important and difficult task. In this work, our aim is to study the verification of such graph transformation, that is how to prove that a graph transformation is correct. Correctness of a graph transformation is more precisely defines as correctness of a specification for the transformation containing additionally a precondition and a postcondition. We decided to use a Hoare-like calculus generating the weakest precondition for a postcondition and a transformation. If this weakest precondition is implied by the actual precondition, the specification is correct. We chose a more algorithmic approach to graph transformation by using atomic actions.We chose to define two ways to build graph transformations: using an imperative programming language and using rule-base rewriting systems. The main ingredient of the verification of graph transformation is the logic that is chosen to represent the precondition, the postcondition and the possible conditions internal to the transformation. So that the logic can interact with the calculus, we require that the decision problem be decidable, that the logic be closed under the substitutions introduced by the Hoare-like calculus and that it has to be able to express the existence and absence of a match for the transformation. The core result of this work is the identification and explanation of these conditions

Les logiques spatiales sont une nouvelle classe de formalismes dedies a la specification des systemes distribues dans la lignee des logiques modales (Hennessy-Milner). Elles peuvent aussi etre vues comme une extension de la logique classique mieux adaptee a la semantique axiomatique des langages imperatifs manipulant des pointeurs, dans la lignee de la logique de Hoare-Floyd. Cette these presente ces diverses logiques en les comparant du point de vue de leur expressivite. On etablit ainsi des encodages des logiques, des fragments minimaux, des unifications de logiques, et des resultats de decidabilite<br>Spatial logics are a new formalism for specifying properties of concurrent systems in the line of modal logics (Hennessy - Milner). They may be seen also as an extension of classical logic better suited for giving an axiomatic semantics for imperative programs manipulating pointers in the line of Hoare-Floyd logic. This thesis present these several issues and compare the different approaches from the point of view of expressiveness. Several encoding, minimal fragments, and decidability results are presented

Dans l'industrie, l'utilisation de l'optimisation est omniprésente. Elle consiste à calculer la meilleure solution tout en satisfaisant un certain nombre de contraintes. Cependant, ce calcul est complexe, long et pas toujours fiable. C'est pourquoi cette tâche est longtemps restée cantonnée aux étapes de conception, ce qui laissait le temps de faire les calculs puis de vérifier que la solution était correcte et si besoin refaire les calculs. Ces dernières années, grâce à la puissance toujours grandissante des ordinateurs, l'industrie a commencé à intégrer des calculs d'optimisation au cœur des systèmes. C'est-à-dire que des calculs d'optimisation sont effectués en permanence au sein du système, parfois des dizaines de fois par seconde. Par conséquent, il est impossible de s'assurer a posteriori de la correction d'une solution ou de relancer un calcul. C'est pourquoi il est primordial de vérifier que le programme d'optimisation est parfaitement correct et exempt de bogue.L'objectif de cette thèse a été de développer outils et méthodes pour répondre à ce besoin.Pour ce faire, nous avons utilisé la théorie de la preuve formelle qui consiste à considérer un programme comme un objet mathématique. Cet objet prend des informations en entrée et produit un résultat. On peut alors, sous certaines conditions sur les entrées, prouver que le résultat satisfait nos exigences. Notre travail a consisté à choisir un programme d'optimisation puis à prouver formellement que le résultat de ce programme est correct<br>In the industry, the use of optimization is ubiquitous. Optimization consists of calculating the best solution subject to a number of constraints. However, this calculation is complex,long and not always reliable. This is why this task has long been confined to the design stages,which allowed time to do the computation and then check that the solution is correct and if necessary redo the computation. In recent years, thanks to the ever-increasing power of computers, the industry has begun to integrate optimization computation at the heart of the systems. That is to say that optimization computation is carried out continuously within the system, sometimes dozens of times per second. Therefore, it is impossible to check a posteriori the solution or restart a calculation. That is why it is important to check that the program optimization is perfectly correct and bug-free. The objective of this thesis was to develop tools and methods to meet this need. To do this we have used the theory of formal proof that is to consider a program as a mathematical object. This object takes input data and produces a result. We can then, under certain conditions on the inputs, prove that the result meets our requirements. Our job was to choose an optimization program and formally prove that the result of this program is correct

Nous présentons d'abord un système théorique permettant la preuve de programmes d'ordre supérieur avec etfets de bord. Ce système est constitué de trois composantes majeures. D'abord un langage de programmation avec un système à effets, avec polymorphisme d'etfets, permettant une analyse fine des effets. Ensuite, un langage de spécitication d'ordre supérieur qui contient aussi un moyen de parler des évolutions d'états. Enfin, un calcul de plus faibles préconditions, permettant d'obtenir, à partir d'un programme annoté, des obligations de preuve, c'est-à-dire des formules dont la validité implique la correction du programme. Nous présentons également deux restrictions du système initial : la première interdit l'aliasing entre régions, ce qui garantit la modularité des spécifications : la deuxième restreint chaque région à un singleton, ne contenant qu'une seule référence. Les deux restrictions permettent de simplifier les obligations générées, mais restreignent l'ensemble des programmes acceptés. Nous présentons une implantation du système théorique. Cet outil repose notamment sur des traductions des obligations de preuve vers la logique d'ordre supérieur et la logique du premier ordre. La première traduction permet notamment l'utilisation de l'assistant de preuve Coq pour valider les obligations de preuve. La traduction vers la logique du premier ordre permet, quant à elle, l'utilisation de démonstrateurs automatiques. Des programmes d'ordre supérieur, entre autres de la bibliothèque standard d'OCaml, sont prouvés correct, ainsi qu'une implémentation à base de continuations de l'algorithme de Koda-Ruskey<br>Ln this thesis, we first present a theoretical system that enables proof of higher-order programs with side effects. This system consists of three major parts. First, a programming language with a traditional type, effect and region system, with effect polymorphism. Second, a higher-order specification language, that also contains a means to describe modifications of the state. Finally, a weakest precondition calcul us that, starting from an annotated program, allows to obtain proof obligations, that is, formulas whose validity implies the correctness of the program w. R. T. Its specification. We also present two restrictions of the initial system. The first disallows region aliasing, obtaining better modularity of the calculus, the second restricts the system to regions that are singleton, containing only a single reference. Both restrictions enable important simplifications that can be applied to proof obligations, but restrict the set of accepted programs. We also present an implementation of this theoretical system, called Who. This tool uses in particular translations of the proof obligations to higher-order logic and first-order logic; these translations are detailed in this thesis. The translation to higher-order logic in particular allows using the Coq proof assistant to validate proof obligations. The translation to first-order logic allows using automated theorem provers. Higher-order programs, found in the standard library of OCaml and elsewhere, have been proved correct using the tool Who, as well as a continuation-based implementation of the Koda-Ruskey algorithm

La modélisation de systèmes biologiques est devenue indispensable pour comprendre les phénomènes complexes et émergents issus d'influences partiellement connues, et pour envisager de contrôler un système altéré dans le but de restaurer un comportement physiologique. Tout modèle, quel que soit son paradigme sous-jacent, fait intervenir des paramètres gouvernant sa dynamique mais les mesures expérimentales ne permettent généralement pas de les identifier et cela reste l'un des problèmes majeurs de la modélisation. Cette thèse propose une méthode automatique d'identification des paramètres dynamiques de systèmes biologiques dans un cadre de modélisation hybride. Le cadre hybride choisi découpe l'espace des phases selon l'activité des entités biologiques, et associe à chacun de ces sous-espaces une vitesse d'évolution de chacun des composants. Nous proposons une logique de Hoare en temps continu ainsi qu'un calcul de plus faible précondition qui, à partir d'observations expérimentales qualitatives et chronométriques, construit les contraintes minimales sur les paramètres du modèle pour qu’il soit compatible avec les observations. Ce calcul mène à un problème de satisfaction de contraintes sur les réels et nous montrons que celui-ci peut être résolu par le solveur AbSolute.Le prototype Holmes BioNet développé au cours de cette thèse peut non seulement automatiser le processus d'identification des valeurs des paramètres à partir des observations expérimentales, mais aussi simuler l'évolution du modèle obtenu afin de le comparer avec les traces expérimentales. Nous utilisons ce prototype pour modéliser le couplage des cycles cellulaire et circadien<br>Modelling biological systems has become instrumental to understand complex and emerging phenomena resulting from partially known influences, and to consider controlling an altered system in order to restore a physiological behaviour. Any model, independent of the underlying paradigm, involves parameters governing its dynamics. However, experimental measurements generally do not allow their identification and this remains one of the major problems of modelling. This PhD proposes an automatic method for identifying the dynamic parameters of biological systems in a hybrid modelling framework. The chosen hybrid framework splits the phase space according to the activity of the biological entities, and associates to each of these subspaces a celerity for each of the components. We introduce a continuous time Hoare logic as well as its weakest precondition calculus which, from qualitative and chronometrical experimental observations, constructs the minimum constraints on the model parameters making it compatible with the observations. This calculus leads to a Constraint Satisfaction Problem on real numbers and we show that it can be solved by the AbSolute solver.The Holmes BioNet prototype developed during this PhD can not only automate the parameter identification process from experimental data, but also simulate the evolution of the obtained model in order to compare it with experimental traces. We use this prototype to model the coupling of the cellular and circadian cycles

Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue.