Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Remarks on abstract Galois theory

This paper is a historical companion to a previous one, in which it was studied the so-called abstract Galois theory as formulated by the Portuguese mathematician José Sebastião e Silva (see da Costa, Rodrigues (2007)). Our purpose is to present some applications of abstract Galois theory to higher-order model theory, to discuss Silva's notion of expressibility and to outline a classical Galois theory that can be obtained inside the two versions of the abstract theory, those of Mark Krasner and of Silva. Some comments are made on the universal theory of (set-theoretic) structures.

The relation between the general maxim of causality and the principle of uniformity in hume's theory of knowledge

ABSTRACT When Hume, in the Treatise on Human Nature, began his examination of the relation of cause and effect, in particular, of the idea of necessary connection which is its essential constituent, he identified two preliminary questions that should guide his research: (1) For what reason we pronounce it necessary that every thing whose existence has a beginning should also have a cause and (2) Why we conclude that such particular causes must necessarily have such particular effects? (1.3.2, 14-15) Hume observes that our belief in these principles can result neither from an intuitive grasp of their truth nor from a reasoning that could establish them by demonstrative means. In particular, with respect to the first, Hume examines and rejects some arguments with which Locke, Hobbes and Clarke tried to demonstrate it, and suggests, by exclusion, that the belief that we place on it can only come from experience. Somewhat surprisingly, however, Hume does not proceed to show how that derivation of experience could be made, but proposes instead to move directly to an examination of the second principle, saying that, "perhaps, be found in the end, that the same answer will serve for both questions" (1.3.3, 9). Hume's answer to the second question is well known, but the first question is never answered in the rest of the Treatise, and it is even doubtful that it could be, which would explain why Hume has simply chosen to remove any mention of it when he recompiled his theses on causation in the Enquiry concerning Human Understanding. Given this situation, an interesting question that naturally arises is to investigate the relations of logical or conceptual implication between these two principles. Hume seems to have thought that an answer to (2) would also be sufficient to provide an answer to (1). Henry Allison, in his turn, argued (in Custom and Reason in Hume, p. 94-97) that the two questions are logically independent. My proposal here is to try to show that there is indeed a logical dependency between them, but the implication is, rather, from (1) to (2). If accepted, this result may be particularly interesting for an interpretation of the scope of the so-called "Kant's reply to Hume" in the Second Analogy of Experience, which is structured as a proof of the a priori character of (1), but whose implications for (2) remain controversial.

The notion of process in nonstandard theory and in Whiteheadian metaphysics

In this article I intend to show that certain aspects of A.N. Whitehead's philosophy of organism and especially his epochal theory of time, as mainly exposed in his well-known work Process and Reality, can serve in clarify the underlying assumptions that shape nonstandard mathematical theories as such and also as metatheories of quantum mechanics. Concerning the latter issue, I point to an already significant research on nonstandard versions of quantum mechanics; two of these approaches are chosen to be critically presented in relation to the scope of this work. The main point of the paper is that, insofar as we can refer a nonstandard mathematical entity to a kind of axiomatical formalization essentially 'codifying' an underlying mental process indescribable as such by analytic means, we can possibly apply certain principles of Whitehead's metaphysical scheme focused on the key notion of process which is generally conceived as the becoming of actual entities. This is done in the sense of a unifying approach to provide an interpretation of nonstandard mathematical theories as such and also, in their metatheoretical status, as a formalization of the empirical-experimental context of quantum mechanics.

Charge transport in disordered materials : simulations, theory, and numerical modeling of hopping transport and electron-hole recombination

Min avhandling behandlar hur oordnade material leder elektrisk ström. Bland materialen som studeras finns ledande polymerer, d.v.s. plaster som leder ström, och mer allmänt organiska halvledare. Av de här materialen har man kunnat bygga elektroniska komponenter, och man hoppas på att kunna trycka hela kretsar av organiska material. För de här tillämpningarna är det viktigt att förstå hur materialen själva leder elektrisk ström. Termen oordnade material syftar på material som saknar kristallstruktur. Oordningen gör att elektronernas tillstånd blir lokaliserade i rummet, så att en elektron i ett visst tillstånd är begränsad t.ex. till en molekyl eller ett segment av en polymer. Det här kan jämföras med kristallina material, där ett elektrontillstånd är utspritt över hela kristallen (men i stället har en väldefinierad rörelsemängd). Elektronerna (eller hålen) i det oordnade materialet kan röra sig genom att tunnelera mellan de lokaliserade tillstånden. Utgående från egenskaperna för den här tunneleringsprocessen, kan man bestämma transportegenskaperna för hela materialet. Det här är utgångspunkten för den så kallade hopptransportmodellen, som jag har använt mig av. Hopptransportmodellen innehåller flera drastiska förenklingar. Till exempel betraktas elektrontillstånden som punktformiga, så att tunneleringssannolikheten mellan två tillstånd endast beror på avståndet mellan dem, och inte på deras relativa orientation. En annan förenkling är att behandla det kvantmekaniska tunneleringsproblemet som en klassisk process, en slumpvandring. Trots de här grova approximationerna visar hopptransportmodellen ändå många av de fenomen som uppträder i de verkliga materialen som man vill modellera. Man kan kanske säga att hopptransportmodellen är den enklaste modell för oordnade material som fortfarande är intressant att studera. Man har inte hittat exakta analytiska lösningar för hopptransportmodellen, därför använder man approximationer och numeriska metoder, ofta i form av datorberäkningar. Vi har använt både analytiska metoder och numeriska beräkningar för att studera olika aspekter av hopptransportmodellen. En viktig del av artiklarna som min avhandling baserar sig på är att jämföra analytiska och numeriska resultat. Min andel av arbetet har främst varit att utveckla de numeriska metoderna och applicera dem på hopptransportmodellen. Därför fokuserar jag på den här delen av arbetet i avhandlingens introduktionsdel. Ett sätt att studera hopptransportmodellen numeriskt är att direkt utföra en slumpvandringsprocess med ett datorprogram. Genom att föra statisik över slumpvandringen kan man beräkna olika transportegenskaper i modellen. Det här är en så kallad Monte Carlo-metod, eftersom själva beräkningen är en slumpmässig process. I stället för att följa rörelsebanan för enskilda elektroner, kan man beräkna sannolikheten vid jämvikt för att hitta en elektron i olika tillstånd. Man ställer upp ett system av ekvationer, som relaterar sannolikheterna för att hitta elektronen i olika tillstånd i systemet med flödet, strömmen, mellan de olika tillstånden. Genom att lösa ekvationssystemet fås sannolikhetsfördelningen för elektronerna. Från sannolikhetsfördelningen kan sedan strömmen och materialets transportegenskaper beräknas. En aspekt av hopptransportmodellen som vi studerat är elektronernas diffusion, d.v.s. deras slumpmässiga rörelse. Om man betraktar en samling elektroner, så sprider den med tiden ut sig över ett större område. Det är känt att diffusionshastigheten beror av elfältet, så att elektronerna sprider sig fortare om de påverkas av ett elektriskt fält. Vi har undersökt den här processen, och visat att beteendet är väldigt olika i endimensionella system, jämfört med två- och tredimensionella. I två och tre dimensioner beror diffusionskoefficienten kvadratiskt av elfältet, medan beroendet i en dimension är linjärt. En annan aspekt vi studerat är negativ differentiell konduktivitet, d.v.s. att strömmen i ett material minskar då man ökar spänningen över det. Eftersom det här fenomenet har uppmätts i organiska minnesceller, ville vi undersöka om fenomenet också kan uppstå i hopptransportmodellen. Det visade sig att det i modellen finns två olika mekanismer som kan ge upphov till negativ differentiell konduktivitet. Dels kan elektronerna fastna i fällor, återvändsgränder i systemet, som är sådana att det är svårare att ta sig ur dem då elfältet är stort. Då kan elektronernas medelhastighet och därmed strömmen i materialet minska med ökande elfält. Elektrisk växelverkan mellan elektronerna kan också leda till samma beteende, genom en så kallad coulombblockad. En coulombblockad kan uppstå om antalet ledningselektroner i materialet ökar med ökande spänning. Elektronerna repellerar varandra och ett större antal elektroner kan leda till att transporten blir långsammare, d.v.s. att strömmen minskar.

Reagan's mythical America : towards a narrative theory of prophetic politics

Lectio praecursoria Tampereen yliopistossa 17.8.2010.

Using an aerial system of remote sensing to detect different nutritional status in Brachiaria decumbens

The aim of this study was to use digital images acquired by cameras attached to a helium balloon to detect variation of the nutritional status in Brachiaria decumbens. The treatments consisted of five doses of nitrogen (0, 50, 100, 150 e 200kg ha-1) with six replications each, evaluated in a completely randomized statistical design. A remote sensing system composed of digital cameras and microcomputers was used for image acquisition, and a helium balloon lifted the cameras to the heights of 15, 20, 25 and 30m. A portable chlorophyll meter and analyses of leaf nitrogen content were used to make comparisons with data obtained by the remote sensing system. Data was acquired in two phases, in different climatic conditions. At the end of each phase, dry matter production was measured. Three vegetation indices were used to evaluate the detection of different nutritional status. The three indices were able to detect the effects of N doses. The indices constructed with the Green spectral band showed to be more efficient.

Geostatistics and remote sensing methods in the classification of images of areas cultivated with citrus

This study compares the precision of three image classification methods, two of remote sensing and one of geostatistics applied to areas cultivated with citrus. The 5,296.52ha area of study is located in the city of Araraquara - central region of the state of São Paulo (SP), Brazil. The multispectral image from the CCD/CBERS-2B satellite was acquired in 2009 and processed through the Geographic Information System (GIS) SPRING. Three classification methods were used, one unsupervised (Cluster), and two supervised (Indicator Kriging/IK and Maximum Likelihood/Maxver), in addition to the screen classification taken as field checking.. Reliability of classifications was evaluated by Kappa index. In accordance with the Kappa index, the Indicator kriging method obtained the highest degree of reliability for bands 2 and 4. Moreover the Cluster method applied to band 2 (green) was the best quality classification between all the methods. Indicator Kriging was the classifier that presented the citrus total area closest to the field check estimated by -3.01%, whereas Maxver overestimated the total citrus area by 42.94%.