Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

Relire les lois du service public, c’est (re)mettre en question le socle des trois principes — égalité, continuité, adaptation constante — solidement établis et largement connus, depuis environ un siècle, comme structurant le régime juridique spécifique de l’ensemble des services publics ; c’est interroger l’actualité de ces principes généraux dans un contexte profondément renouvelé et, à travers elle, la pérennité du service public lui-même, en tant qu’objet juridique. Afin de dresser pareil bilan de santé, deux niveaux de relecture sont retenus. Il s’agit, en premier lieu, de revenir sur l’ensemble théorique que constituent aujourd’hui les lois d’égalité, de continuité et d’adaptation constante : ces dernières, devenues subsidiaires par rapport aux impératifs économique et gestionnaire, ne semblent plus être des données de premier ordre dans le système de pensée juridique des services publics ; elles continuent toutefois d’assurer l’unité de la notion de service public, notion réduite à la portion congrue. Il s’agit, en deuxième lieu, de reconsidérer chacune des lois séparément, dans son contenu : la signification respective des trois principes classiques a évolué et de « nouveaux principes » sont recherchés, ceux-ci n’étant pour l’essentiel que des déclinaisons plus ou moins nouvelles de ceux-là ; une tendance à leur subjectivisation est observable sans devoir être exagérée, les lois du service public continuant d’exprimer l’esprit objectiviste du service public. / Reviewing the laws of public service means questioning the foundation of the three principles — equality, continuity, mutability — that have been firmly rooted and widely known, for about a century, as structuring the specific legal regime of all public services. It also means questioning the developments of these general principles in a profoundly renewed context and, through it, the durability of the public service itself, as a legal object. To do so, two review levels are employed. On the one hand, we have to go back over the theoretical set of the laws of equality, continuity and mutability, which have become subsidiary to economic and managerial imperatives and as such no longer seem to be the most important considerations in the legal thought system of public services. However, they continue to ensure the unity of the notion of public service, a notion reduced to its bare bones. On the other hand, we have to reconsider each of the laws separately, in their content. The respective meanings of the three principles have changed and « new principles » are being sought, these being essentially newer variations of those. A tendency to give more consideration to the individuals involved when applying the laws can be observed but must not be exaggerated, as the laws of public service are continuing to express the objectivist spirit of the public service.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Ce document présente une méthode de dérivation automatique des spécifications algébriques vers un langage impératif. Par langage impératif nous désignons un langage de programmation ``traditionnel'' avec déclarations des variables (état) et dont les programmes sont des suites d'instructions qui modifient l'état. L'instruction caractéristique est l'affectation destructrice d'une valeur à une variable. Une spécification algébrique est composée de sortes, de constructeurs qui définissent l'ensemble des valeurs atteignables (que l'on peut dénoter), et d'opérateurs axiomatisés par des équations conditionnelles orientées. Nous définissons un lien d'implémentation entre les objets du domaine abstrait des spécifications algébriques et ceux du domaine concret des programmes impératifs. Ce lien permet de paramétrer la dérivation d'une spécification. L'implémentation des opérateurs respecte le choix de la forme de dérivation et celui de la bibliothèque importée. Elle résout les conflits d'accès aux variables et minimise les coûts en recopies de valeurs engendrées par le passage du fonctionnel à l'impératif. De manière analogue au lien d'implémentation entre une spécification algébrique et un programme impératif, nous définissons un lien d'implémentation dite abstraite entre les sortes et constructeurs de deux spécifications algébriques. Nous proposons pour les constructeurs, soit d'effectuer une dérivation systématique en un type de donnée impératif, soit de calculer les liens d'implémentation abstraite potentiels vers les sortes dont les implémentations des constructeurs sont réutilisables. Une méthode de transformation de la spécification algébrique est enfin proposée, qui favorise les modifications ``en-place'' de données, dans une variante de la méthode de dérivation précédente.

L’analyse des injonctions en polonais est placée dans une perspective pragmatico-énonciative. L’injonction est définie comme un acte illocutoire directif qui vise l’accomplissement ou le non accomplissement de l’action par l’allocutaire. L’auteur de ce travail part du constat qu’il n’existe pas de forme d’énoncé qui véhicule en soi la valeur injonctive. Seule l’actualisation d’un énoncé dans un contexte donné permet de définir la valeur injonctive qui se présente comme un continuum allant de l’injonction douce à l’injonction catégorique. Cela suppose une interaction entre la situation d’énonciation, divers marqueurs sémantico-syntaxiques, métainformatifs, expressifs ainsi que la prise en compte des facteurs extralinguistiques. Le concept de l’injonction permet de constater la suprématie du critère fonctionnel (le but de l’injonction) par rapport au critère purement formel (la structure de l’injonction). La notion d’honorification offre un cadre de description capable de rendre compte des différences qui existent entre le domaine non distant et le domaine distant ce qui conduit à établir une hiérarchie entre divers emplois injonctifs. / The analysis of the injunctions in Polish is carried out within the pragmatic and enunciation theoretical framework. The injunction is defined as an illocutionary directive act which aims at the fulfillment or non-fulfillment of the action by the hearer. The author starts by presupposing that there is no shape of statement which conveys in itself the injunctive value. Only the actualizing of a statement in a given context allows to define the injunctive value which appears as a continuum going from soft injunction to categorical injunction. The actualizing in question asks for combination and interaction between the situation of speaking, the various semantic, syntactic, meta-informative and expressive markers, and the taking into account of the extra-linguistic factors. The concept of injunction allows to notice the supremacy of the functional criterion (the purpose of the injunction) over the purely formal criterion (the structure of the injunction). The notion of honorification offers a frame of description allowing to acknowledge the differences between the not-distant domain and the distant domain, which leads to establishing a hierarchy between diverse injunctive uses.

D’un point de vue syntaxique, la phrase impérative possède des caractéristiques saillantes qui lui sont propres. Cette étude vise à reconstituer sa structure pour comprendre son fonctionnement. Je propose un arbre syntaxique où la projection du sujet est présente pour héberger un sujet phonétiquement absent avec des propriétés grammaticales et sémantiques. La périphérie gauche de l’impératif demeure inchangée. Les projections verbales sont morphologiquement appauvries : temps absent et personne appauvrie. Cependant, dans certaines langues, la projection aspectuelle joue un rôle important. Une caractéristique de l’impératif qui a été étudiée par de nombreux chercheurs est le placement du clitique. Les données démontrent que les pronoms clitiques objets sont derrière le verbe impératif (enclitiques) comparativement à la phrase déclarative où les clitiques sont devant le verbe (proclitiques). Finalement, le registre de langue agit non seulement sur ce placement des clitiques, mais aussi sur leur forme. / From a syntactic point of view, the imperative clause presents some salient characteristics. This study tries to reconstitute its structure to understand the mechanics at work. I propose a syntactic tree in which the subject projection is present hosting a phonetically null subject with grammatical and semantic properties. The left periphery of the imperative clause reveals no change. As for the verbal projections, they are morphologically meagre : lack of tense and impoverishment of the person. However, in some languages, the aspectual projection plays an important role. A characteristic of the imperative that many searchers had worked on is the clitic placement. The data shows that the pronominal object clitics take place after the imperative verb (enclitics) as opposed to the declarative clause in which the clitics take place before the verb (proclitics). Finally, the language register acts not only on the clitic placement, but also on their form.

Nous avons organisé notre travail d'après la sémantique d'une phrase type esli p, q, en commençant par les conditionnelles, modèle le plus fréquent. Organisée d'après le type de connecteur qui apparaît dans ces constructions, notre présentation expose les caractéristiques de chaque variante conditionnelle prise séparément. Nous proposons comme base de cette thèse une classification des types de condition en 4 groupes : • condition potentielle • condition irréelle • condition virtuelle • condition réelle Ainsi, la Ie partie est consacrée aux conditionnelles proprement dites et aux hypothétiques avec esli qui réalisent les trois premiers types de condition. Cette partie traite des caractéristiques particulières de ces phrases, de la spécificité de leur construction et de leur fonctionnement. Un chapitre à part est consacré à l'usage des synonymes lexicaux de esli en russe moderne. La IIe partie est centrée sur d'autres variantes conditionnelles. Il s'agit des phrases asyndétiques sans connecteur. Cette partie comprend également les phrases où le rôle du connecteur est assuré par un lexème ou forme grammaticale qui, en soi, n'est pas spécialisé dans l'expression de la condition (l'impératif, stoit, tol'ko, ljuboj, etc.). Ces phrases représentent des synonymes syntaxiques des phrases avec esli. Enfin, la IIIe partie comprend les conditionnelles secondaires, où l'expression de la condition n'est pas mise au premier plan, et les factuelles. Dans le premier cas, il s'agit des itératives, véhiculant une condition réelle. Les déductives et concessives, elles, se trouvent à la limite des conditionnelles et des factuelles. Quant aux factuelles, phrases de mise en relief et phrases oppositives, elles ne sont jamais hypothétiques, mais elles partagent avec les conditionnelles la structure commune du type esli p, q. La présentation de l'ensemble des phrases du type esli p, q permet de montrer une certaine unité où le modèle central est constitué par les conditionnelles.

Ce mémoire présente plusieurs définitions de sémantiques formelles et de transformations de programmes, et expose les choix de conception associés. En particulier, ce mémoire décrit une transformation de programmes inspirée de l'évaluation partielle et dédiée à la compréhension de programmes scientifiques écrits en Fortran. Il détaille également le front-end d'un compilateur réaliste du langage C, ayant été formellement vérifié en C.

Les langages synchrones sont apparus autour des années quatre-vingt, en réponse à un besoin d'avoir un modèle mathématique simple pour implémenter des systèmes temps réel critiques. Dans ce modèle, le temps est découpé en instants discrets durant lesquels tous les composants du système reçoivent et produisent une donnée. Cette modélisation permet des raisonnements beaucoup plus simples en évitant de devoir prendre en compte le temps de calcul de chaque opération. Dans le monde du logiciel critique, la fiabilité du matériel et de son fonctionnement sont primordiaux, et on accepte d'être plus lent si on devient plus sûr. Afin d'augmenter cette fiabilité, plutôt que de concevoir manuellement tout le système, on utilise des machines qui synthétisent automatiquement le système souhaité à partir d'une description la plus concise possible. Dans le cas du logiciel, ce mécanisme s'appelle la compilation, et évite des erreurs introduites par l'homme par inadvertance. Elle ne garantit cependant pas la bonne correspondance entre le système produit et la description donnée. Des travaux récents menés par une équipe INRIA dirigée par Xavier Leroy ont abouti en 2008 au compilateur CompCert d'un sous-ensemble large de C vers l'assembleur PowerPC pour lequel il a été prouvé dans l'assistant de preuve Coq que le code assembleur produit correspond bien à la description en C du programme source. Un tel compilateur offre des garanties fortes de bonne correspondance entre le système synthétisé et la description donnée. De plus, avec les compilateurs utilisés pour le temps réel critique, la plupart des optimisations sont désactivées afin d'éviter les erreurs qui y sont liées. Dans CompCert, des optimisations elles aussi prouvées sont proposées, ce qui pourrait permettre ces passes dans la production de systèmes temps réel critiques sans en compromettre la fiabilité. Le but de cette thèse est d'avoir une approche similaire mais spécifique à un langage synchrone, donc plus approprié à la description de systèmes temps réel critiques que ne l'est le C. Un langage synchrone flots de données semblable à Lustre, nommé Ls, et un langage impératif semblable au langage C, nommé Obc y sont proposés ainsi que leur sémantique formelle et une chaîne de compilation avec des preuves de préservation de sémantique le long de cette chaîne.