The goal of this thesis is the development of support for test generation and animation based on object-oriented specifications. We aim particularly to take advantage of state-of-the-art satisfiability solving techniques by using an appropriate representation of object-oriented data. While automated test generation seeks a large set of data to execute an implementation on, animation performs computations that comply with a specification based on user-provided input data. Animation is a valuable technique for validating specifications.As a foundation of this work, we present clarifications and a partial formalization of the Object Constraint Language (OCL) as well as some extensions in order to allow for test generation and animation based on OCL specifications.For test generation, we have implemented several enhancements to HOL-TestGen, a tool built on top of the Isabelle theorem proving system that generates tests from specifications in Higher-Order Logic (HOL). We show how SMT solvers can be used to solve various types of constraints in HOL and present a modular approach to case splitting for deriving test cases. The latter facilitates the introduction of splitting rules that are tailored to object-oriented specifications.For animation, we implemented the tool OCLexec for animating OCL specifications. OCLexec generates from operation contracts corresponding Java implementations that call an SMT-based constraint solver at runtime.

Bien que les contextes d'écriture d'Isabelle Eberhardt et de Bernard Moitessier comptent plusieurs différences, un certain nombre de correspondances peuvent être relevées, du fait que leurs récits élaborent une poétique du dehors ancrée dans l'immensité géographique. Leur rapport aux espaces désertique et océanique soulève une même question : comment habiter l'immensité? Isabelle Eberhardt a voyagé à travers le désert du Sahara entre 1897 et 1904. Elle a poursuivi son « rêve du vieil Orient resplendissant », consignant dans ses cahiers des impressions, des nouvelles, etc., jusqu'à sa mort dans l'inondation d'Aïn Sefra. Grâce au travail éditorial de Marie-Odile Delacour et de Jean-René Huleu, ses Écrits sur le sable, appartenant aux littératures suisse, française et maghrébine, paraissent en 1988. Bernard Moitessier est un navigateur français du XXe siècle né en Indochine, dont les récits de voyage Vagabond des mers du sud, Cap Horn à la voile et La longue route racontent des traversées océaniques effectuées entre 1952 et 1969. C'est plus particulièrement son dernier récit, qui retrace les étapes d'un tour du monde et demi à la voile, en solitaire, en doublant les caps de Bonne-Espérance, Leeuwin et Horn, qui fera l'objet de notre attention. Nos analyses visent à contribuer à la réception littéraire des Écrits sur le sable et des récits de voyage en voilier de Moitessier, qui demeurent à ce jour peu étudiés. Dans le premier chapitre, nous procédons à un survol théorique des éléments de définition que propose la critique du récit de voyage. Nous recourons également aux notions d'altérité, d'exotisme et de transfuge afin de montrer que la manière dont l'espace est vécu par les voyageurs influence leur écriture. Le deuxième chapitre présente l'approche géopoétique du récit de voyage. Après un bref survol de ce qu'est la géopoétique, nous structurons l'analyse des récits d'Eberhardt et de Moitessier selon trois principes, soit la critique radicale, l'appel du dehors et le mouvement. Ce dernier s'inscrit notamment dans les cartes qui accompagnent les œuvres de notre corpus. Le récit déplie la carte, mais la modalité et les conditions du parcours influencent et parfois troublent la perception des paysages. Nous exposons dans le troisième chapitre quelques éléments constitutifs du désert et de l'océan, afin de souligner leurs différences géographiques et leurs ressemblances, notamment sur le plan de l'imaginaire. Ces deux espaces convoquent la dimension du sacré et du mythe tout en suscitant un désir de contemplation face à l'immensité. Ainsi, le nouveau rapport au monde se développe chez Isabelle Eberhardt grâce à l'acte de paysage, déclenché par le rythme des jeux de lumière sur les ergs et les regs sahariens, tandis que chez Bernard Moitessier, la dynamique de l'habiter s'opère grâce à la fusion entre le navigateur et son bateau. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Isabelle Eberhardt, Bernard Moitessier, récit de voyage, géopoétique, immensité, paysage, désert, océan, Écrits sur le sable, La longue route.

Thesis (M.A.) -- State University College at Buffalo, 2006. / Includes bibliographical references (p. 103-113).

Zugl.: Bremen, Univ., Diss., 2005

Techn. University, Diss., 2002--München.

Texte remanié de: Proefschrift--Rijksuniversiteit te Utrecht, 1993. / Bibliogr. p. 311-323. Index.

Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software. This thesis presents USIMPL, a component of the Orca project for formal verification that builds on Foster’s Isabelle/UTP with features of Schirmer’s Simpl in order to achieve a modular, scalable framework for deductive proofs of program correctness utilizing Hoare logic and Hoare-style algebraic laws of programming. / Master of Science / Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software (OSes, compilers, and similar programs that have a high level of complexity but work on a lower level than typical user applications such as text editors, image viewers, and the like). This thesis presents USIMPL, a component of the Orca project for formal verification that builds on an existing framework for computer-aided, deductive mathematical proofs (Foster’s Isabelle/UTP) with features inspired by a simple but featureful language used for verification (Schirmer’s Simpl) in order to achieve a modular, scalable framework for proofs of program correctness utilizing the rule-based mathematical representation of program behavior known as Hoare logic and Hoare-style algebraic laws of programming, which provide a formal methodology for transforming programs to equivalent formulations.

Dans ce mémoire, je donne un aperçu de ma perception de ce qui m'entoure et de la manière dont j'aborde le monde à travers ma pratique artistique. Mes déplacements sur le territoire se font à l'intérieur de sites et de paysages que je m'approprie avec la photographie. Je travaille à partir de parcelles extraites du réel, des fragments issus du champ visuel et physique existant, et j'exploite leur effacement partiel à l'aide de la surexposition et du traitement des images. Le brouillage résultant advient également et inévitablement pour moi dans le souvenir que j'ai de mes prises de vue. Une fois que j'ai quitté les lieux photographiés, je m'en fais une représentation paysagère qui s'éloigne déjà du vécu in situ. Je reconstruis dès lors, à partir de cette nouvelle réalité brouillée et fragmentaire, quelque chose de concret et de praticable, qui permettra un renouvellement de l'expérience par le corps. Je travaille mes constructions en intégrant des vestiges de territoire, donnant ainsi une forme renouvelée à l'espace et au temps dont ils se sont dissociés dans la mémoire et l'acte photographique. De cette façon, je prends concrètement part au chantier cyclique du construit, de l'effacement et de ce qui les relie.

La dialectique instruit-elle les arts plastiques? C’est par la relation entre deux éléments majeurs de notre culture et de nos usages que nous proposons une réponse : sujet et objet, de tensions en renversements, font l’originalité d’oeuvres européennes et nord-américaines depuis les années soixante. Leur rencontre débute par un face à face puis glisse vers un renversement, où la chose physique transformée en un matériau vivant prend la place du sujet traditionnellement acteur de son environnement. Elle acquiert une dimension nouvelle lorsque le public y joue un rôle, d’interlocuteur à participant. L'artiste français Philippe Ramette crée des objets d’un nouveau genre pour accomplir des déplacements dignes de la quatrième dimension. L’autrichien Erwin Wurm forme le corps humain en une «sculpture d'une minute» quand un homme colle sa poitrine à un tabouret de bois. Le peintre et écrivain Guy de Cointet met en scène une histoire de sujets et d’objets à Los Angeles dans les années soixante-dix. C’est enfin une affaire de point de vue sur de précieuses choses, de décor incarné que la française Isabelle Cornaro instaure. Dans ce carré de plasticiens, la dialectique, sous diverses qualités, est en jeu : si elle est à l’origine définie comme un art de discussion ou une méthode d'interprétation, outil d’une pensée critique, nous soutenons qu’elle est ici la base d’un processus en art, capable d’éclairer un ensemble d’œuvres de notre temps et d'aborder sous un angle nouveau l’univers de ses créateurs. / Does the dialectic inform the visual arts? By the relation between two major elements of our culture and our uses we propose an answer : subject and object, of tensions in inversions, make the originality of European and North-American works since the sixties. Their meeting begins by face to face then slips into a twist, gaining a new dimension when the public plays a mere part. The physical thing, transformed into a living material, takes the place of the subject usualy actor of its environment. French artist Philippe Ramette creates objects of a fourth type to achieve improbable movements. Austrian sculptor Erwin Wurm transforms the human body into a « one minute sculpture » as a man sticks his chest to a wood stool. French painter and writer Guy de Cointet directs an history of subjects and objects on stage in the Los Angeles in the seventies. It is finally a work about our point of view on invaluable things, of incarnated «décor» that Isabelle Cornaro sets up. In this square of artists, the dialectic, under various qualities, is in stake : if we define it literally as an art of discussion or method for critical thought, we support that it is here the base of a process in contemporary art, able to clarify works of our time and threw new light on the world of its creators.

La thèse a pour objet l'étude approfondie d'une série de huit tableaux monumentaux intitulée "Les Festivités du papegai en 1615 à Bruxelles". Exceptionnelle par le type de sujet et par le format, cette série fut commandée par les archiducs Albert et Isabelle (1598-1621) à leur peintre Denijs van Alsloot (1568 ?-1625/26) afin de célébrer la victoire de l'infante au tir de l'oiseau de bois (le "papegai") du Grand Serment des arbalétriers à Bruxelles. Elle est aujourd’hui incomplète, mais la confrontation des sources écrites avec les tableaux subsistants (en ce compris quelques répliques et variantes) permet d’établir qu’elle se composait à l'origine de six toiles ayant pour objet l’Ommegang communal – qui eut lieu le 31 mai 1615 et fut placé sous le signe de l’exploit de l’infante –, d’une peinture représentant "Isabelle tirant l’oiseau", et d’une toile montrant une "Fête au Vivier d’Oie en présence des archiducs", dans la forêt domaniale de Soignes. <p> Sans doute en raison de leur aspect descriptif, les tableaux conservés n'ont jamais été soumis à une analyse qui prenne en compte leur spécificité artistique, la plupart des chercheurs s'étant contentés jusqu'à présent d'examiner les spectacles dépeints dans une perspective historique. La thèse propose dès lors une étude qui non seulement repose sur une analyse des sources écrites et cherche à identifier les motifs représentés, mais aussi explore les composantes formelles, techniques et conventionnelles des peintures. Ceci afin, précisément, de mieux définir le rapport entre l’image donnée et la réalité des faits historiques. Car si les "Festivités" n'ont nullement valeur de reportage, leur raison d’être n’en a pas moins été de témoigner par le menu détail de certains événements. Et c’est très exactement la nature de ce témoignage, formulé avec les moyens propres à la peinture, qui est au cœur du questionnement. <p> La thèse se compose de deux parties. Dans la première partie, l'attention est portée sur la vie et la production de Denijs van Alsloot en général. Le peintre avait en effet été peu ou mal étudié jusqu’à présent. Or, de toute évidence, une meilleure connaissance de l’ensemble des activités artistiques de Van Alsloot permet d’aborder avec plus de justesse l’étude des "Festivités". Plusieurs éléments de la carrière de l'artiste furent en outre déterminants dans le choix d’Albert et Isabelle de faire appel à ses services pour la réalisation de la série. <p> La seconde partie se concentre sur l'examen des "Festivités". Le premier chapitre fait le point sur ce que les archives nous apprennent à propos de la commande et de l’historique des peintures originales comme des répliques et des variantes. Le second chapitre analyse la technique et le style de chacun des tableaux. Il vise également à reconstituer les étapes préparatoires dans la réalisation des peintures et à définir la nature des rapports entre les tableaux du point de vue de l’exécution. Une attention particulière est en outre portée à l'intervention comme sous-traitant du peintre Antoon Sallaert (1594-1650). <p> La signification politique des tableaux constitue le thème du troisième chapitre. Sont étudiés d'abord les circonstances historiques qui amenèrent Isabelle à participer au tir du Grand Serment et la cour à commander la série peinte des "Festivités". Le cadre d’origine des toiles est examiné ensuite, afin de mesurer l’influence potentielle de ce cadre sur la forme et le contenu des œuvres. Car si celles-ci contiennent une foule de renseignements valables sur les célébrations, il n’en demeure pas moins qu’il ne peut s’agir d’images objectives. Les "Festivités" servaient des intentions particulières qui ont amené les artistes à opérer des choix et à soumettre les scènes à des structures iconographiques signifiantes. C’est donc à déchiffrer et à interpréter la "rhétorique de l'image" que la thèse s'attache en dernier lieu. <p> En définitive, par la réévaluation d'un type particulier d'iconographie politique, l'auteure de la thèse espère contribuer aux travaux toujours plus nombreux sur le rôle de l'image dans l'élaboration du discours princier.