Letteratura scientifica selezionata sul tema "Filtrage par motif"

La transformation de programmes est une pratique très courante dans le domaine des sciences informatiques. De la compilation à la génération de tests en passant par de nombreuses approches d'analyse de codes et de vérification formelle des programmes, c'est un procédé qui est à la fois omniprésent et crucial au bon fonctionnement des programmes et systèmes informatiques. Cette thèse propose une étude formelle des procédures de transformation de programmes dans le but d'exprimer et de garantir des propriétés syntaxiques sur le comportement et les résultats d'une telle transformation. Dans le contexte de la vérification formelle des programmes, il est en effet souvent nécessaire de pouvoir caractériser la forme des termes obtenus par réduction suivant une telle transformation. En s'inspirant du modèle de passes de compilation, qui décrivent un séquençage de la compilation d'un programme en étapes de transformation minimales n'affectant qu'un petit nombre des constructions du langage, on introduit, dans cette thèse, un formalisme basé sur les notions de filtrage par motif et de réécriture permettant de décrire certaines propriétés couramment induites par ce type de transformations. Le formalisme proposé se repose sur un système d'annotations des symboles de fonction décrivant une spécification du comportement attendu des fonctions associées. On présente alors une méthode d'analyse statique permettant de vérifier que les transformations étudiées, exprimées par un système de réécriture, satisfont en effet ces spécifications
Program transformation is an extremely common practice in computer science. From compilation to tests generation, through many approaches of code analysis and formal verification of programs, it is a process that is both ubiquitous and critical to properly functionning programs and information systems. This thesis proposes to study the program transformations mechanisms in order to express and verify syntactical guarantees on the behaviour of these transformations and on their results.Giving a characterisation of the shape of terms returned by such a transformation is, indeed, a common approach to the formal verification of programs. In order to express some properties often used by this type of approaches, we propose in this thesis a formalism inspired by the model of compilation passes, that are used to describe the general compilation of a program as a sequence of minimal transformations, and based on the notions of pattern matching and term rewriting.This formalism relies on an annotation mechanism of function symbols in order to express a set of specfications describing the behaviours of the associated functions. We then propose a static analysis method in order to check that a transformation, expressed as a term rewrite system, actually verifiesits specifications

Les assistants de preuve basés sur des théories des types dépendants sont de plus en plus utilisé comme un outil pour développer programmes certifiés. Un exemple réussi est l'assistant de preuves Coq, fondé sur le Calcul des Constructions Inductives (CCI). Coq est un langage de programmation fonctionnel dont un expressif système de type qui permet de préciser et de démontrer des propriétés des programmes dans une logique d'ordre supérieur. Motivé par le succès de Coq et le désir d'améliorer sa facilité d'utilisation, dans cette thèse nous étudions certaines limitations des implémentations actuelles de Coq et sa théorie sous-jacente, CCI. Nous proposons deux extension de CCI que partiellement resourdre ces limitations et que on peut utiliser pour des futures implémentations de Coq. Nous étudions le problème de la terminaison des fonctions récursives. En Coq, la terminaison des fonctions récursives assure la cohérence de la logique sous-jacente. Les techniques actuelles assurant la terminaison de fonctions récursives sont fondées sur des critères syntaxiques et leurs limitations apparaissent souvent dans la pratique. Nous proposons une extension de CCI en utilisant un mécanisme basé sur les type pour assurer la terminaison des fonctions récursives. Notre principale contribution est une preuve de la normalisation forte et la cohérence logique de cette extension. Nous étudions les définitions par filtrage dans le CCI. Avec des types dépendants, il est possible d'écrire des définitions par filtrage plus précises, par rapport à des langages de programmation fonctionnels Haskell et ML. Basé sur le succès des langages de programmation avec types dépendants, comme Epigram et Agda, nous développons une extension du CCI avec des fonctions similaires.

Les systemes de preuves bases sur les theories des types offrent un cadre uniforme qui permet de programmer, specifier et prouver. L'utilisateur dispose d'un langage de programmation, d'un langage de specification et d'outils qui l'aident a raisonner formellement sur son programme. Dans le but de rapprocher dans ces systemes la syntaxe des definitions de fonctions de celle des mathematiques et des langages de programmation a la ml, nous etudions les preuves de terminaison de fonctions recursives definies equationnellement. A partir de la methode de synthese de preuves proposee par gilles dowek pour les systemes de types purs, et celle proposee par hassan saidi pour le systeme t de godel, nous proposons une methode de synthese de preuves pour le calcul des constructions inductives (cci). Ce calcul est une theorie des types tres riche, avec types polymorphes, types dependants et types inductifs primitifs (par exemple, les types algebriques et les predicats inductifs). Cette methode est complete, et fournit un cadre general ou definir des strategies de recherche de preuves. La completude se paye par la non terminaison. Nous etudions donc des restrictions qui terminent et qui permettent de resoudre une certaine classe de problemes de filtrage et d'unification du second ordre dans cci. Nous analysons aussi la derivation de principes d'analyse par cas specialises (dits principes d'inversion), technique necessaire pour resoudre une classe large de problemes de filtrage. Ces restrictions, que l'on peut considerer comme des algorithmes de compilation, synthetisent des preuves explicites a partir de notations plus implicites, dans l'esprit de la compilation des motifs dans un langage fonctionnel. Ceci permet d'incorporer au langage de specification du systeme de preuves la notation par filtrage de motifs aussi bien pour ecrire des programmes que des preuves.

Dans les dernières années XML est devenu un véritable modèle de bases de données permettant de représenter, stocker et échanger des données semi-structurées. Il est devenu alors nécessaire de développer des langages de requêtes efficaces pour ce modèle. Différents langages de requêtes existent qui utilisent une primitive de déconstruction dans le but de capturer des parties de documents XML, qui peuvent êtes vus comme des arbres. Il existe deux déconstructeurs : (i) la navigation par chemins qui permet de naviguer en profondeur (par des projections) à l'intérieur d'un arbre afin de capturer un sous-arbre (XPath), (ii)le filtrage par motifs qui permet de capturer en largeur différents sous-arbres (XDuce, CDuce). L'objectif de cette thèse est d'offrir au langage CDuce un langage de requêtes déclaratif, qui puisse tirer parti du typage fort et statique de CDuce. Ce langage de requêtes (appelé CQL) est formellement défini et permet d'utiliser et de combiner en une requête les deux déconstructeurs, dans le but d'écrire des requêtes concises et expressives. Partant du postulat que le filtrage par motifs est plus performant que la navigation descendante, nous donnons une traduction optimisante qui réécrit toutes les projections d'une requête en motifs. Cette traduction et d'autres optimisations ont été validées par des jeux de tests et des "microbenchmarks", ainsi que comparées avec d'autres moteurs de requêtes. L'écriture de requêtes avec motifs pouvant être laborieux pour un utilisateur non averti, une interface graphique (appelée PBE) est proposée qui permet de faciliter cette écriture en étant guidée par les types de la DTD.

Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes.

Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes
In software engineering, type systems are often considered in order to prevent the occurrence of meaningless terms in regard to a type specification. When extending a given programming language with new dedicated features, the typing of these features must be compatible with the ones in the host language. This thesis is situated in the context of term rewriting embedded in object-oriented programming and aims to develop a safe type system featuring subtyping for the support of associative pattern matching on algebraic terms built from variadic operators. In this work we consider the Tom rewriting language that provides associative pattern matching constructs and rewrite strategies for Java. We describe Tom code evaluation through the definition of the operational semantics of the Tom language as an essential element to show that the type system is safe. The type system includes type checking and constraint-based type inference. The constraint language is composed of equality constraints solved by unification and subtyping constraints solved by a combination of simplification, generation of solution and garbage collecting. The type system was integrated in Tom which provides both stronger expressiveness and more safety able to ensure that the transformations described by rewrite rules preserve the type of terms

Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes
In software engineering, type systems are often considered in order to prevent the occurrence of meaningless terms in regard to a type specification. When extending a given programming language with new dedicated features, the typing of these features must be compatible with the ones in the host language. This thesis is situated in the context of term rewriting embedded in object-oriented programming and aims to develop a safe type system featuring subtyping for the support of associative pattern matching on algebraic terms built from variadic operators. In this work we consider the Tom rewriting language that provides associative pattern matching constructs and rewrite strategies for Java. We describe Tom code evaluation through the definition of the operational semantics of the Tom language as an essential element to show that the type system is safe. The type system includes type checking and constraint-based type inference. The constraint language is composed of equality constraints solved by unification and subtyping constraints solved by a combination of simplification, generation of solution and garbage collecting. The type system was integrated in Tom which provides both stronger expressiveness and more safety able to ensure that the transformations described by rewrite rules preserve the type of terms

Esta dissertação de mestrado aborda formulações computacionais e algoritmos para a busca e extração de padrões em cadeias biológicas. Em particular, o presente texto concentra-se nos dois problemas a seguir, considerando-os sob as distâncias de Hamming e Levenshtein: a) como determinar os locais nos quais um dado padrão ocorre de modo aproximado em uma cadeia fornecida; b) como extrair padrões que ocorram de modo aproximado em um número significativo de cadeias de um conjunto fornecido. O primeiro problema, para o qual já existem diversos algoritmos polinomiais, tem recebido muita atenção desde a década de 60, e ganhou novos ares com o advento da biologia computacional, nos idos dos anos 80, e com a popularização da Internet e seus mecanismos de busca: ambos os fenômenos trouxeram novos obstáculos a serem superados, em razão do grande volume de dados e das bastante justas restrições de tempo inerentes a essas aplicações. O segundo problema, de surgimento um pouco mais recente, é intrinsicamente desafiador, em razão de sua complexidade computacional, do tamanho das entradas tratadas nas aplicações mais comuns e de sua dificuldade de aproximação. Também é de chamar a atenção o seu grande potencial de aplicação. Neste trabalho são apresentadas formulações adequadas dos problemas abordados, assim como algoritmos e estruturas de dados essenciais ao seu estudo. Em especial, estudamos a extremamente versátil árvore dos sufixos, assim como uma de suas generalizações e sua estrutura irmã: o vetor dos sufixos. Grande parte do texto é dedicada aos filtros baseados em q-gramas para a busca aproximada de padrões e algumas de suas mais recentes variações. Estão cobertos os algoritmos bit-paralelos de Myers e Baeza-Yates-Gonnet para a busca de padrões; os algoritmos de Sagot para a extração de padrões; os algoritmos de filtragem de Ukkonen, Jokinen-Ukkonen, Burkhardt-Kärkkäinen, entre outros.
This thesis deals with computational formulations and algorithms for the extraction and search of patterns from biological strings. In particular, the present text focuses on the following problems, both considered under Hamming and Levenshtein distances: 1. How to find the positions where a given pattern approximatelly occurs in a given string; 2. How to extract patterns which approximatelly occurs in a certain number of strings from a given set. The first problem, for which there are many polinomial time algorithms, has been receiving a lot of attention since the 60s and entered a new era of discoveries with the advent of computational biology, in the 80s, and the widespread of the Internet and its search engines: both events brought new challenges to be faced by virtue of the large volume of data usually held by such applications and its time constraints. The second problem, much younger, is very challenging due to its computational complexity, approximation hardness and the size of the input data usually held by the most common applications. This problem is also very interesting due to its potential of application. In this work we show computational formulations, algorithms and data structures for those problems. We cover the bit-parallel algorithms of Myers, Baeza-Yates-Gonnet and the Sagots algorithms for patterns extraction. We also cover here the oustanding versatile suffix tree, its generalised version, and a similar data structure: the suffix array. A significant part of the present work focuses on q-gram based filters designed to solve the approximate pattern search problem. More precisely, we cover the filter algorithms of Ukkonen, Jokinen-Ukkonen and Burkhardt-Kärkkäinen, among others.