Thèse (M.A.)--Université Laval, 1996. / Bibliogr.: f. 115-127. Publié aussi en version électronique.

Thesis (Ph.D.)--Northwestern University, 1997. / Source: Dissertation Abstracts International, Volume: 58-04, Section: A, page: 1152. Adviser: Paul Edwards.

Maîtrise--Histoire de la photographie--Paris 4, 2001. / Bibliogr. p. 161-172.

Thèse (M.A.)--Université Laval, 1997. / Bibliogr.: f. 33. Publié aussi en version électronique.

A biform theory is a combination of an axiomatic theory and an algorithmic theory. It is used to integrate reasoning and computation in a common theory and can include algorithms with precisely specified input-output relationships. Isabelle is one of the leading interactive theorem provers. Isabelle includes locales, a module system that uses theory morphisms to manage theory hierarchies, and that has a rich and extensive library with multiple useful proof and formalization techniques. A case study of eight biform theories of natural number arithmetic is described in the paper “Formalizing Mathematical Knowledge as a Biform Theory Graph” by J. Carette and W. M. Farmer. The biform theories form a graph linked by theory morphisms. Seven of the biform theories are in first-order logic and one is in simple type theory. The purpose of this thesis is to test how a theory graph of biform theories can be formalized in Isabelle by attempting to formalize this case study. We work with locales and sublocales in Isabelle to formalize the test case. The eight biform theories are defined as regular axiomatic theories, while the algorithms are functions defined on inductive types representing the syntax of the theories. / Thesis / Master of Science (MSc)

Thesis (Ph. D.)--Florida State University, 2004. / Advisor: Dr. Aimee Boutin, Florida State University, College of Arts and Sciences, Dept. of Modern Languages and Linguistics. Title and description from dissertation home page (viewed July 12, 2004). Includes bibliographical references.

München, Techn. University, Diss., 2003.

En posant le regard sur deux figures emblématiques du théâtre et du cinéma, choisies délibérément, Gérard Philipe et Isabelle Huppert, il ne s’agit pas d’un discours généraliste, ni d’une théorie sur l’acteur, mais plutôt de s’appuyer sur leurs traces en essayant d’analyser les interviews recueillis dans les principaux supports médiatiques qui tentent de dévoiler leur personnalité et l’idéal vers lequel ils tendent, sachant que tous deux émergent après des évènements historiques majeurs : d’un côté la fin de la seconde guerre mondiale laissant une France dévastée en quête d’égérie dont Gérard Philipe sera l’exemple, de l’autre mai 1968 et ses bouleversements au niveau des mœurs, amenant à l’avènement de la nouvelle vague. Le défi à relever fut de comparer un acteur disparu il y a plus d’un demi-siècle avec une actrice contemporaine. Leur grande maturité professionnelle s’est avérée déterminante dans la poursuite des concepts qu’ils défendent. Leur recherche personnelle est perceptible au travers de l’évolution de leur carrière et laisse indéniablement un écho médiatique, pouvant se rapprocher d’une dimension mythologique de l’acteur.Il est ici question d’une analyse comparative pour tenter de comprendre comment leur personnalité qui caractérise leur jeu, entre réserve et don de soi, intuition et réflexion, leur a permis d’enchaîner les rôles tout au long de leur vie en alternant le théâtre et le cinéma. / Considering two deliberately selected figureheads of the theatre and of the cinema, Gérard Philipe and Isabelle Huppert, the purpose is not to draw up a general speech, or a theory on the actor, but rather to rely on their tracks and try to analyze the main media interviews attempting to unveil their personality and expectations amidst major historical events : on one hand, the end of World War 2 with a devastated France in pursuit of a new inspiring spirit that will be embodied by Gérard Philipe, and, on the other hand, (the students' revolution of) May 1968 with drastic changes in standards of behaviour that will lead to the coming of "The New Wave".The challenge was to compare an actor, who left us half a century ago, with a contemporary actress. Their great professional maturity proved to be the determining factor towards their ideal.Their personal research appears through the evolution of their career and undoubtedly leaves a media echo that can be linked to the mythological dimension of the actor.The question is to analyze and compare to try and understand how their personality, characterizing their way of acting, between reserve and self giving, intuition and reflection, allowed them, throughout their life, to play one part after the other, alternately for the theatre and the cinema.

Le test à base de modèle, en particulier test basé sur des assistants à la preuve, réduit de façon transparente l'écart entre la théorie, le modèle formel, et l’implémentation d'un système informatique. Actuellement, les techniques de tests offrent une possibilité d'interagir directement avec de "vrais" systèmes : via différentes propriétés formelles, les tests peuvent être dérivés et exécutés sur le système sous test. Convenablement, l'ensemble du processus peut être entièrement automatisé. Le but de cette thèse est de créer un environnement de test de séquence à base de modèle pour les programmes séquentiels et concurrents. Tout d'abord une théorie générique sur les monades est présentée, qui est indépendante de tout programme ou système informatique. Il se trouve que notre théorie basée sur les monades est assez expressive pour couvrir tous les comportements et les concepts de tests. En particulier, nous considérons ici : les exécutions séquentielles, les exécutions concurrentes, les exécutions synchronisées, les exécutions avec interruptions. Sur le plan conceptuel, la théorie apporte des notions comme la notion raffinement de test, les cas de tests abstraits, les cas de test concrets, les oracles de test, les scénarios de test, les données de tests, les pilotes de tests, les relations de conformités et les critères de couverture dans un cadre théorique et pratique. Dans ce cadre, des règles de raffinement de comportements et d'exécution symbolique sont élaborées pour le cas générique, puis affinées et utilisées pour des systèmes complexes spécifique. Comme application pour notre théorie, nous allons instancier notre environnement par un modèle séquentiel d'un microprocesseur appelé VAMP développé au cours du projet Verisoft. Pour le cas d'étude sur la concurrence, nous allons utiliser notre environnement pour modéliser et tester l'API IPC d'un système d'exploitation industriel appelé PikeOS.Notre environnement est implémenté en Isabelle / HOL. Ainsi, notre approche bénéficie directement des modèles, des outils et des preuves formelles de ce système. / Formal methods can be understood as the art of applying mathematical reasoningto the modeling, analysis and verification of computer systems. Three mainverification approaches can be distinguished: verification based on deductive proofs,model checking and model-based testing.Model-based testing, in particular in its radical form of theorem proving-based testingcite{brucker.ea:2012},bridges seamlessly the gap between the theory, the formal model, and the implementationof a system. Actually,theorem proving based testing techniques offer a possibility to directly interactwith "real" systems: via differentformal properties, tests can be derived and executed on the system under test.Suitably supported, the entire process can fully automated.The purpose of this thesis is to create a model-based sequence testing environmentfor both sequential and concurrent programs. First a generic testing theory basedon monads is presented, which is independent of any concrete program or computersystem. It turns out that it is still expressive enough to cover all common systembehaviours and testing concepts. In particular, we consider here: sequential executions,concurrent executions, synchronised executions, executions with abort.On the conceptual side, it brings notions like test refinements,abstract test cases, concrete test cases,test oracles, test scenarios, test data, test drivers, conformance relations andcoverage criteria into one theoretical and practical framework.In this framework, both behavioural refinement rules and symbolic executionrules are developed for the generic case and then refined and used for specificcomplex systems. As an application, we will instantiate our framework by an existingsequential model of a microprocessor called VAMP developed during the Verisoft-Project.For the concurrent case, we will use our framework to model and test the IPC API of areal industrial operating system called PikeOS.Our framework is implemented in Isabelle/HOL. Thus, our approach directly benefitsfrom the existing models, tools, and formal proofs in this system.

Les langages de spécifications basés et orientés objets (comme UML/OCL, JML, Spec#, ou Eiffel) permettent la création et destruction, la conversion et tests de types dynamiques d'objets statiquement typés. Par dessus, les invariants de classes et les opérations de contrat peuvent y être exprimés; ces derniers représentent les éléments clés des spécifications orientées objets. Une sémantique formelle des structures de données orientées objets est complexe : des descriptions imprécises mènent souvent à différentes interprétations dans les outils qui en résultent. Dans cette thèse, nous démontrons comment dériver un environnement de preuves moderne comme un méta-outil pour la définition et l'analyse de sémantique formelle de langages de spécifications orientés objets. Étant donné une représentation d'un langage particulier plongé en Isabelle/HOL, nous construisons pour ce langage un environnement étendu d'Isabelle, à travers une méthode de génération de code particulière, qui implique notamment plusieurs variantes de génération de code. Le résultat supporte l'édition asynchrone, la vérification de types, et les activités de déduction formelle, tous "hérités" d'Isabelle. En application de cette méthode, nous obtenons un outil de modélisation orienté objet pour du UML/OCL textuel. Nous intégrons également des idiomes non nécessairement présent dans UML/OCL --- en d'autres termes, nous développons un support pour des dialectes d'UML/OCL à domaine spécifique. En tant que construction méta, nous définissons un méta-modèle d'une partie d'UML/OCL en HOL, un méta-modèle d'une partie de l'API d'Isabelle en HOL, et une fonction de traduction entre eux en HOL. Le méta-outil va alors exploiter deux procédés de générations de code pour produire soit du code raisonnablement efficace, soit du code raisonnablement lisible. Cela fournit donc deux modes d'animations pour inspecter plus en détail la sémantique d'un langage venant d'être plongé : en chargeant à vitesse réelle sa sémantique, ou simplement en retardant à un autre niveau "méta" l'expérimentation précédente pour un futur instant de typage en Isabelle, que ce soit pour des raisons de performances, de tests ou de prototypages. Remarquons que la génération de "code raisonnablement efficace", et de "code raisonnablement lisible" incluent la génération de code tactiques qui prouvent une collection de théorèmes formant une théorie de types de données orientés objets d'un modèle dénotationnel : étant donné un modèle de classe UML/OCL, les preuves des propriétés pertinentes aux conversions, tests de types, constructeurs et sélecteurs sont traitées automatiquement. Cette fonctionnalité est similaire aux paquets de théories de types de données présents au sein d'autres prouveurs de la famille HOL, à l'exception que certaines motivations ont conduit ce travail présent à programmer des tactiques haut-niveaux en HOL lui-même. Ce travail prend en compte les plus récentes avancées du standard d'UML/OCL 2.5. Par conséquent, tous les types UML/OCL ainsi que les types logiques distinguent deux éléments d'exception différents : invalid (exception) et null (élément non-existant). Cela entraîne des conséquences sur les propriétés aussi bien logiques qu'algébriques des structures orientées objets résultant des modèles de classes. Étant donné que notre construction est réduite à une séquence d'extension conservative de théorie, notre approche peut garantir la correction logique du langage entier considéré, et fournit une méthodologie pour étendre formellement des langages à domaine spécifique. / Object-based and object-oriented specification languages (likeUML/OCL, JML, Spec#, or Eiffel) allow for the creation and destruction, casting and test for dynamic types of statically typed objects. On this basis, class invariants and operation contracts can be expressed; the latter represent the key elements of object-oriented specifications. A formal semantics of object-oriented data structures is complex: imprecise descriptions can often imply different interpretations in resulting tools. In this thesis we demonstrate how to turn a modern proof environment into a meta-tool for definition and analysis of formal semantics of object-oriented specification languages. Given a representation of a particular language embedded in Isabelle/HOL, we build for this language an extended Isabelle environment by using a particular method of code generation, which actually involves several variants of code generation. The result supports the asynchronous editing, type-checking, and formal deduction activities, all "inherited" from Isabelle. Following this method, we obtain an object-oriented modelling tool for textual UML/OCL. We also integrate certain idioms not necessarily present in UML/OCL --- in other words, we develop support for domain-specific dialects of UML/OCL. As a meta construction, we define a meta-model of a part of UML/OCL in HOL, a meta-model of a part of the Isabelle API in HOL, and a translation function between both in HOL. The meta-tool will then exploit two kinds of code generation to produce either fairly efficient code, or fairly readable code. Thus, this provides two animation modes to inspect in more detail the semantics of a language being embedded: by loading at a native speed its semantics, or just delay at another "meta"-level the previous experimentation for another type-checking time in Isabelle, be it for performance, testing or prototyping reasons. Note that generating "fairly efficient code", and "fairly readable code" include the generation of tactic code that proves a collection of theorems forming an object-oriented datatype theory from a denotational model: given a UML/OCL class model, the proof of the relevant properties for casts, type-tests, constructors and selectors are automatically processed. This functionality is similar to the datatype theory packages in other provers of the HOL family, except that some motivations have conducted the present work to program high-level tactics in HOL itself. This work takes into account the most recent developments of the UML/OCL 2.5 standard. Therefore, all UML/OCL types including the logic types distinguish two different exception elements: invalid (exception) and null (non-existing element). This has far-reaching consequences on both the logical and algebraic properties of object-oriented data structures resulting from class models. Since our construction is reduced to a sequence of conservative theory extensions, the approach can guarantee logical soundness for the entire considered language, and provides a methodology to soundly extend domain-specific languages.