Cette thèse se place dans le cadre des méthodes formelles et plus précisément dans celui de la vérification déductive et du système Why3. Ce dernier fournit un ensemble d'outils pour la spécification, l'implémentation et la vérification à l'aide de démonstrateurs externes. Why3 propose en particulier un langage de programmation adapté à la preuve, appelé WhyML. Un aspect important de ce langage est le code fantôme, à savoir des éléments de programme introduits exclusivement pour les besoins de la spécification et de la preuve. Pour obtenir un code exécutable, le code fantôme est éliminé par un processus automatique appelé extraction. L'une des contributions principales de cette thèse est la formalisation et l'implémentation du mécanisme d'extraction deWhy3. La formalisation consiste à montrer que le programme extrait préserve la sémantique du programme de départ, en s'appuyant notamment sur un système de types avec effets. Ce mécanisme d'extraction a été utilisé avec succès pour obtenir plusieurs modules OCaml corrects par construction, dans le cadre d'une bibliothèque vérifiée de structures de données et d'algorithmes. Cet effort de preuve a conduit à deux autres contributions de cette thèse.La première est une technique systématique pour la vérification de structures avec pointeurs, à l'aide de modèles du tas délimités.Une preuve entièrement automatique d'une structure union-find a pu être obtenue grâce à cette technique. La seconde contribution est un moyen de spécifier un algorithme d'itération indépendamment de son implémentation. Plusieurs curseurs et itérateurs d'ordre supérieur ont été spécifiés et vérifiés en utilisant cette approche. / This thesis is set in the field of formal methods, more precisely in the domain of deductive program verification. Our working context is the Why3 framework, a set of tools to implement, formally specify, and prove programs usingoff-the-shelf theorem provers. Why3 features a programming language,called WhyML, designed with verification in mind. An important feature of WhyML is ghost code: portions of the program that are introduced for the sole purpose of specification andverification. When it comes to get an executable implementation, ghost code is removed by an automatic process called extraction. One of the main contributions of this thesis is the formalization and implementation of Why3's extraction. The formalization consists in showing that the extracted program preserves the same operational behavior as the original source code, based on a type and effect system. The new extraction mechanism has been successfully used to get correct-by-construction OCaml modules, which are part of averified OCaml library of data structures and algorithms. This verification effort led to two other contributions of this thesis.The first is a systematic approach to the verification ofpointer-based data structures using ghost models of fragments of the heap. A fully automatic verification of a union-find data structure was achieved using this technique. The second contribution is a modular way to reason about iteration, independently of the underlying implementation. Several cursors and higher-orderiterators have been specified and verified with this approach.

Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code. / This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs.

Denna systematiska litteraturstudie syftar till att undersöka hur induktiva eller deduktivaarbetssätt i undervisning påverkar elevers förståelse för matematiska innehåll samt vilka föroch nackdelar det finns med respektive. Studiens frågeställningar grundar sig i egnaerfarenheter och utifrån observation på skolor, där vi mött elever med bristande matematiskförståelse. Vi har då uppmärksammat att lärare återkommande fokuserar undervisningen påutantillkunskap, och i hög grad bearbetar matematiska innehåll med deduktiva arbetssätt.Observationerna utgjorde grunden till en hypotes om att det finns ett samband mellan eleversbristande förståelse och deduktiv undervisning som fokuserar på utantillkunskap. I studiengranskas tidigare forskning genom att tio utvalda vetenskapliga artiklar kategoriseras utifrånteoretiska perspektiv och dess innehåll tematiseras utifrån framgångsfaktorer för eleverslärande. Studiens resultat med utgångspunkt i de granskade artiklarna tyder på attarbetssättets induktiva eller deduktiva karaktär är av mindre betydelse för eleversmatematiska förståelse. Slutsatsen blir således att de identifierade framgångsfaktorerna ärmer adekvata för elevers matematiska förståelse.

We propose to replace Zadeh's DeMorgan-type negation in fuzzy logic by a Heyting-type negation which, unlike the former, preserves the law of the excluded contradiction and is more in line with negation in databases and logic programs. We show that the resulting system can be used for obtaining conservative extensions of relational and deductive databases (resp. normal logic programs).

We define a preferential semantics based on stable generated models for a very general class of temporal deductive databases. We allow two kinds of temporal information to be represented and queried: timepoint and timestamp formulas, and show how each of them can be translated into the other. Because of their generality, our formalism and our semantics can serve as a basis for comparing and extending other temporal deductive database frameworks.

Economists have convulsively maintained the assumption that humans are able to arrive at decisions by perfect deductive rationality, despite the fact empirical evidences are showing otherwise. The contradicting evidences have resulted in a personal view that instead of finding a unified theory about decision-making, a sound approach would be to study how humans in fact are reasoning in specific contexts. The context of interest for this paper is where it could be assumed humans’ persistence of acting rational is determined by the perceived burden of the problem. In this work, the inductive way of arriving at decisions plays an important role, and the paper will present a way of describing this process in a consistent way. The process will be denoted as the actual level of behavioral change, and represent the core property of this paper. Applying the presented theory is most appropriate for situations where it could be assumed the burden of a problem, expressed as a prevalence rate, will drive the behavioral change. The line of reasoning in this paper will therefore be applied to the important arena of fighting the spread of HIV.

The role of grammar in the teaching of foreign languages has been extensivelydiscussed over the years, and nowadays the literature shows a growing acceptanceof grammar as an important part of the communicative approach. However,according to our experience and what can be gleaned from research, student perceivegrammar as difficult, abstract, and boring - which often negatively affects theirmotivation to learn a foreign language.In this context, the question we need to consider is: what is the best way to teachgrammar? The purpose of this research paper is to delve into the attitudes of studentsregarding the inductive and the deductive teaching methods, what aspects of thesemethods favour or hinder their motivation, as well as which is, according to them,the best way to work with grammar in the classroom.The methodology employed was a mini-experiment in which two approaches weretrialled, inductive and deductive, to then measure attitudes by means of a survey(questionnaire), followed by further details via a complementary interview andmeasuring learning effectiveness through exit tickets. Informants were drawn fromtwo groups of Spanish language students (9th grade elective Spanish).The results obtained indicate a clear preference toward the deductive method,although they also hint to most positive outcomes from a combination of bothmethods (inductive and deductive). About the factors that influence motivation,those standing out were the possibility of working in a group as well as theimportance of offering tasks with adequate difficulty levels, as those perceived astoo difficult have negative consequences in terms of motivation

This study explored the relationships between roughly 330 participants' tolerance of ambiguity and their preference for either an inductive or deductive presentation of grammar by means of an online survey. Most participants were college students. Other variables examined included years of study, in-country experience, proficiency, age, year in school, and language of choice. A new instrument for measuring inductive vs. deductive preference was also created based on Cohen, Oxford, and Chi's (2001) Learning Style Survey (LSS). Results showed weak correlations between: tolerance of ambiguity and inductive preference (.25), tolerance of ambiguity and proficiency (.25), and inductive preference and proficiency (.20). Additional findings include: a correlation (.62) between proficiency and years of instruction received, a slight correlation (.22) between age and tolerance of ambiguity, no correlation between years of language instruction and tolerance of ambiguity, no correlation between studying abroad and ambiguity tolerance or inductive/deductive preference, and no correlation between age and inductive vs. deductive preference. Lastly, data was analyzed to determine whether language was a contributing factor or not, and only the participants learning Japanese were significantly different (p = .004), with a higher preference for inductive learning.

Despite the increased use of criminal profiling by law enforcement agencies, few studies examine factors impacting profile accuracy, and only one has evaluated profiler training. The present study examined the efficacy of profiler training on profile accuracy for sexual homicide offenders. Participants (N = 198) were randomly assigned to the training or control condition. Participants in the training condition learned inductive and deductive profiling techniques for sexual homicide offenders, whereas control participants learned about sexual violence prevention. Results indicated that participants’ self-reported use of combined profiling methods produced more accurate profiles. Differences between gender and training groups were also present. These findings suggest brief psychology-based training can be used to teach police officers and detectives to more accurately identify and apprehend criminals.

Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions. / This thesis comes within the domain of proofs of programs by deductive verification. The deductive verification generates from a program source and its specification a mathematical formula whose validity proves that the program follows its specification. The program source describes what the program does and its specification represents what the program should do. The validity of the formula is mainly verified by automatic provers. During the last ten years separation logic has shown to be an elegant way to deal with programs which use data-structures with pointers. However it requires a specific logical language, provers, and specific reasoning techniques.This thesis introduces a technique to express ideas from separation logic in the traditional framework of deductive verification. Unfortunately the mathematical formulas produced are not in the same first-order logic than the ones of provers. Thus this work defines new conversions between the polymorphic first-order logic and the many-sorted logic used by most proves.The first part of this thesis leads to an implementation in the Jessietool. The second part results in an important participation to the writing of the Why3 tool, in particular in the architecture and writing of the transformations which implement these conversions.