1 Einleitung, 2 Formale Theorien für Programmiersprachen, 3 HOARE-Logik für while-Programme, 4 Ausblick

Whereas early researchers in computability theory described effective computability in terms of such models as Turing machines, Markov algorithms, and register machines, a recent trend has been to use simple programming languages as computability models. A parallel development to this programming approach to computability theory is the current interest in systematic and scientific development and proof of programs. This paper investigates the feasibility of using formal proofs of programs in computability theory. After describing a framework for formal verification of programs written in a simple theoretical programming language, we discuss the proofs of several typical programs used in computability theory.

No description available.

[pt] Atualmente, a maioria dos programas para computadores é obtida através da WEB. Como muitas vezes a procedência são fontes desconhecidas, é preciso se certificar de que o código se comporta como o esperado. A solução ideal seria verificar o código contra uma especificação de políticas de segurança ,contudo, isso pode consumir muito tempo.Uma outra alternativa é fazer com que o próprio código prove ser seguro. O conceito de proof-carryng code (PCC)é baseado nessa idéia : um programa carrega consigo uma prova de sua conformidade com certas políticas de segurança. Ou seja ,ele carrega uma prova a respeito de propriedades do próprio código. Portanto, os mesmos métodos froamsi usados para a verificação de programs podem se utilizados para esta tecnolgia. Considerando este fato,neste trabalho é estudado como cálculo de Hoare, em método formal para realizar a verificação de programas, aplicado a códigos-fonte escritos em uma linguagem de programação imperativa, pode ser útil á tecnica de PCC. Conseqüentemente, são pesquisados métodos para a geração de provas de correção de programas utilizando o método citado, para tornar possível a geração de provas de segurança para PCC utilizando o cálculo de Hoare. / [en] Nowdays most computer programs are obtained from the WEB. Since their source is usually unknown, it is necessary to be sure that the code of the program behaves as expected.The ideal solution would be verify the code against a specification of safety policies.However, this can take too much time.Another approach is making the code itself prove that it is safe. The concept os proof-carryng code (PCC) is based on this idea: a program carries a proof of its conformity with certain safety policies. That is , it carries a proof cencerning properties related to the code itself. Therefore, the same formal methods employed in formal verification of programs can be used in this tecnology. Due to this fact, in this work it is studied how Hoare logic applied to source codes written in an imperative programming language, which is a formal methods are researched to generate proofs of program correctness using the method explained, so that it can be possible to generate PCC safety programs with Hoare logic.

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. / 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.

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.

During the Geological Survey of Canada’s Cumberland Peninsula Integrated Geoscience project a ~150km long NE-SW trending volcanic belt, now termed the North Touak-Cape Dyer volcanic belt, was mapped. The volcanic rocks that comprise the belt are dominantly green weathering komatiitic rocks with some black weathering tholeiitic occurrences. Given the similar stratigraphic position, textures, mineralogy, and geochemical characteristics of the volcanic rocks throughout the belt they have been termed the Totnes Road formation, after the locality from which they were first described. The komatiitic rocks possess numerous unusual characteristics for ultramafic volcanic rocks including: fragmental textures, lack of spinifex texture, young eruption age (Paleoproterozoic), eruption through ancient continental crust, and enrichment in the HFSEs including the REEs. This places them in the uncommon and poorly understood sub-type of komatiites termed Karasjok-type komatiites. Given the ultramafic nature of the rocks and their within-plate geochemical signatures, a mantle plume is the most likely source of these rocks, with the komatiites being sourced from the hot plume axis and the tholeiites from the cooler plume head. Incorporation and melting of mantle enriched by the addition of subduction zone recycled, garnet-bearing eclogitic material, beneath thick lithosphere could cause the rocks geochemical enrichment. Stratigraphically overlying the Totnes Road formation is a variety of chemical sedimentary rocks including chert, sulphide and silicate facies iron formation, and sulphide-rich boulders. Given their consistent stratigraphic position and parallel REE patterns, these rocks have been interpreted as a co-genetic suite and are grouped under the Clephane Bay formation, after a locality that exposes a spectacular section of the chemical rocks. The variety of lithologies is believed to be due to mixing of hydrothermal and detrital inputs during deposition within an anoxic basin. Regional correlations in the area are tentative due to the lack of available geochronological and geochemical data. Mafic-ultramafic volcanic occurrences to both the north and the south of the Cumberland Peninsula show remarkably similar geochemical characteristics to the Totnes Road formation. Thus it is possible that one plume was the source for numerous volcanic occurrences within in the region but more detailed study is required to prove or disprove this possibility.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-01-20T20:41:23Z No. of bitstreams: 1 EvandoCarlosPessini_TESE.pdf: 1797248 bytes, checksum: e3b1bb46971f452029930068e9f8babf (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-01-21T18:18:20Z (GMT) No. of bitstreams: 1 EvandoCarlosPessini_TESE.pdf: 1797248 bytes, checksum: e3b1bb46971f452029930068e9f8babf (MD5) / Made available in DSpace on 2016-01-21T18:18:20Z (GMT). No. of bitstreams: 1 EvandoCarlosPessini_TESE.pdf: 1797248 bytes, checksum: e3b1bb46971f452029930068e9f8babf (MD5) Previous issue date: 2014-07-29 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior - CAPES / Esta tese apresenta um m?todo de certifica??o de composi??es de servi?os web sem?nticos, o qual visa assegurar estaticamente sua corre??o funcional. O m?todo de certifica??o consiste em duas dimens?es de verifica??o, denominadas base e funcional. A dimens?o base ? centrada na verifica??o da correta aplica??o dos servi?os web sem?nticos na composi??o, i.e., visa certificar que as invoca??es de servi?o especificadas na composi??o est?o em conformidade com as respectivas defini??es dos servi?os. A certifica??o desta dimens?o explora a compatibilidade sem?ntica entre os argumentos dados na invoca??o e os par?metros formais do servi?o web sem?ntico. A dimens?o funcional visa certificar que a composi??o cumpre uma dada especifica??o expressa na forma de pr? e p?s-condi??es. Esta dimens?o ? formalizada atrav?s de um c?lculo baseado na l?gica de Hoare. Especifica??es de corre??o parciais envolvendo composi??es de servi?os web sem?nticos podem ser derivadas a partir do sistema dedutivo proposto. Este trabalho caracteriza-se tamb?m por explorar o emprego de um fragmento da l?gica descritiva, i.e., ALC, para expressar as especifica??es de corre??o parciais. Como forma de operacionalizar o m?todo de certifica??o, foi desenvolvido um ambiente de suporte para a defini??o das composi??es de servi?os web sem?nticos, assim como os mecanismos necess?rios para realizar a certifica??o. O m?todo de certifica??o foi avaliado experimentalmente atrav?s da aplica??o em tr?s provas de conceito diferentes. As provas de conceito desenvolvidas possibilitaram avaliar de forma ampla o m?todo de certifica??o proposto / This thesis presents a certification method for semantic web services compositions which aims to statically ensure its functional correctness. Certification method encompasses two dimensions of verification, termed base and functional dimensions. Base dimension concerns with the verification of application correctness of the semantic web service in the composition, i.e., to ensure that each service invocation given in the composition comply with its respective service definition. The certification of this dimension exploits the semantic compatibility between the invocation arguments and formal parameters of the semantic web service. Functional dimension aims to ensure that the composition satisfies a given specification expressed in the form of preconditions and postconditions. This dimension is formalized by a Hoare logic based calculus. Partial correctness specifications involving compositions of semantic web services can be derived from the deductive system proposed. Our work is also characterized by exploiting the use of a fragment of description logic, i.e., ALC, to express the partial correctness specifications. In order to operationalize the proposed certification method, we developed a supporting environment for defining the semantic web services compositions as well as to conduct the certification process. The certification method were experimentally evaluated by applying it in three different proof concepts. These proof concepts enabled to broadly evaluate the method certification

Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project. / Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet.