Refactoring is the process of reorganising or restructuring code by means of behaviour-preserving program transformations, themselves called refactorings. Most modern development environments come with built-in support for refactoring in the form of automated refactorings that the user can perform at the push of a button. Implementing refactorings is notoriously complex, however, and even state-of-the-art implementations have very low standards of correctness and can introduce subtle changes of behaviour into refactored programs. In this thesis, we develop concepts and techniques that make it possible to give concise, modular specifications of refactorings. These specifications are precise enough to cover all details of the object language, and thus give rise to full featured, high-quality refactoring implementations. Their modularity, on the other hand, makes them amenable to formal proof, and hence opens the door to the rigorous verification of refactorings. We discuss a disciplined approach to maintaining name bindings and avoiding name capture by treating the binding from a name to the declaration it refers to as a dependency that the refactoring has to preserve. This approach readily generalises to other types of dependencies for capturing control flow, data flow and synchronisation behaviour. To implement complex refactorings, it is often helpful for the refactoring to internally work on a richer language with language extensions that make the transformation easier to express. We show how this allows the decomposition of refactorings into small microrefactorings that can be specified, implemented and verified in isolation. We evaluate our approach by giving specifications and implementations of many commonly used refactorings that are concise, yet match the implementations in the popular Java development environment Eclipse in terms of features, and outperform them in terms of correctness. We give detailed informal correctness proofs for some of our specifications, which are greatly aided by their modular structure. Finally, we discuss a rigorous formalisation of the central name binding framework used by most of our specifications in the theorem prover Coq, and show how its correctness can be established mechanically.

The lack of a method for developing programs from Z specifications is a difficulty that is now widely recognised. As a contribution to solving this problem, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. Other refinement techniques have been proposed for Z; ZRC builds upon some of them, but distinguishes itself in that it is completely formalised. As several other refinement techniques, ZRC is formalised in terms of weakest preconditions. In order to define the semantics of its language, ZRC-L, we construct a weakest precondition semantics for Z based on a relational semantics proposed by the Z standards panel. The resulting definition is not unexpected, but its construction provides evidence for its suitability and, additionally, establishes connections between predicate transformers and two different relational models. The weakest precondition semantics of the remaining constructs of ZRC-L justify several assumptions that permeate the formalisation of Morgan's refinement calculus. Based on the semantics of ZRC-L, we derive all laws of ZRC. Typically the refinement of a schema in ZRC begins with the application of a conversion law that translates it to a notation convenient for refinement, and proceeds with the application of refinement laws. The conversion laws of ZRC formalise the main strategies and rules of translation available in the literature; its set of refinement laws is extensive and includes support for procedures, parameters, recursion, and data refinement. Morgan and Back have proposed different formalisations of procedures and parameters in the context of refinement techniques. We investigate a surprising and intricate relationship between these works and the substitution operator that renames the free variables of a program, and reveal an inconsistency in Morgan's calculus, Back's approach does not suffer from this inconsistency, but he does not present refinement laws. We benefit from both works and use a model based on Back's formalism to derive refinement laws similar to those in Morgan's calculus. Furthermore, we derive additional laws that formalise Morgan's approach to recursion. Three case studies illustrate the application of ZRC. They show that ZRC can be useful as a technique of formal program development, but are by no means enough to ascertain the general adequacy of its conversion and refinement laws. Actually, since Z does not enforce a specific style of structuring specifications, it is likely that new laws will be proved useful for particular system specifications: two of our case studies exemplify this situation. Our hope is that ZRC and its formalisation will encourage further investigation into the refinement of Z specifications and the proper justification of any emerging strategies or techniques.

Specifications are necessary for communicating decisions and intentions and for documenting results at many stages of the program development process. Informal specifications are typically used today, but they are imprecise and often ambiguous. Formal specifications are precise and exact but are more difficult to write and understand. We present work aimed toward enabling the practical use of formal specifications in program development, concentrating on the Clear language for structured algebraic specification. Two different but equivalent denotational semantics for Clear are given. One is a version of a semantics due to Burstall and Goguen with a few corrections, in which the category-theoretic notion of a colimit is used to define Clear's structuring operations independently of the underlying 'institution' (logical formalism). The other semantics defines the same operations by means of straightforward set-theoretic constructions; it is not institutionindependent but it can be modified to handle all institutions of apparent interest. Both versions of the semantics have been implemented. The settheoretic implementation is by far the more useful of the two, and includes a parser and typechecker. An implementation is useful for detecting syntax and type errors in specifications, and can be used as a front end for systems which manipulate specifications. Several large specifications which have been processed by the set-theoretic implementation are presented. A semi-automatic theorem prover for Clear built on top of the Edinburgh LCF system is described. It takes advantage of the structure of Clear specifications to restrict the available information to that which seems relevant to proving the theorem at hand. If the system is unable to prove a theorem automatically the user can attempt the proof interactively using the high-level primitives and inference rules provided. We lay a theoretical foundation for the use of Clear in systematic program development by investigating a new notion of the implementation of a specification by a lower-level specification. This notion extends to handle parameterised specifications. We show that this implementation relation is transitive and commutes with Clear's structuring operations under certain conditions. This means that a large specification can be refined to a program in a gradual and modular fashion, where the correctness of the individual refinements guarantees the correctness of the resulting program.

Diss. (sammanfattning) Linköping : Univ., 2004. / Härtill 4 uppsatser.

Diss. (sammanfattning) Stockholm : Karol. inst., 2006. / Härtill 4 uppsatser.

[pt] O principal objetivo deste trabalho é desenvolver um sistema computacional, denominado SDP, para auxiliar a elaboração de programas baseados no Método dos Elementos Finitos (MEF). É dividido em três partes: primeiramente é apresentado o SDP, que compreende um sistema de gerenciamento de dados (memória principal, arquivos em disco e fita), uma padronização para a documentação e facilidades para testes e depuração de programas; em uma segunda parte, utilizando-se este sistema, é desenvolvida uma organização para os programas e para as bibliotecas de rotinas; finalmente, são apresentadas aplicações mostrando as principais características do sistema e sua potencialidade. Os problemas de elasticidade infinitesinal linear, condução de calor e elasto-plasticidade incremental são descritos através de uma formulação variacional, a partir da qual são desenvolvidas soluções aproximadas utilizando-se o MEF. Por último, tomando-se por base as soluções encontradas por meio desta abordagem, são elaborados os programas aplicativos. / [en] The main purpose of this work is to develop a computational system, denominated SDP, to aid the elaboration of Finite Element Method (FEM) programs. This work is divided in three parts: initially is presented the SDP that comprises a data management system (main memory, disc file and tapes), a standardization for the documentation and facilities for program testing and debugging. In the second part, a program and a routines library organization are developed using this computational system. Finally, applications showing the main characteristics and capacity of the SDP are presented. The problems of Linear Infinitesimal Elasticity, Heat Transfer and Incremental Elastic Plasticity are described by a variational formulation. Based on the variational theory approximated solutions are developed by means of the FEM. The last step is the applicative program elaboration using the solutions achieved by this approach.

Como reflexo do aumento da incidência de câncer no país, uma alta proporção de pacientes recebem alta hospitalar com diagnóstico de câncer no Hospital das Clínicas da Faculdade de Medicina da Universidade de São Paulo. Por essa razão, a necessidade de um sistema de informações para a coleta, armazenamento e análise dos dados relativos aos pacientes com câncer atendidos na instituição se tornou bastante crítica para o registro do câncer do HC-FMUSP. Neste projeto de mestrado, realizamos uma avaliação das necessidades do grupo e detectamos a necessidade de criar um instrumento de informática que fosse complementar ao programa já em uso da Função Oncocentro de São Paulo, mas que também pudesse ser usado isoladamente. Isso foi feito tendo em conta uma reavaliação de todos os processos envolvidos com a coleta de dados relativos aos pacientes, desde a identificação deles até o resultado dos tratamentos envolvidos. A construção do instrumento abrangeu o ciclo de vida do sistema, desde o diagnóstico do ambiente, desenvolvimento dos projetos lógico e físico, programação e implantação. Esse sistema ainda está em teste, mas produtos como o boletim do RHC-FMUSP atesta que ele funciona a contento. / Possibly as a reflection of the cancer incidence increase in Brazil, a high proportion of patients are discharged from the Hospital das Clínicas da Faculdade de Medicina da Universidade de São Paulo with the diagnosis of cancer. For this reason, the development of a system of information became critical in order to collect and analyse the amount of data stored by Cancer Registry at HCFMUSP. In this study, we first evaluated the needs of the cancer registry personnel and developed an software to support these needs as a complement of the active program in use. This instrument should be used alone if necessary. All processes were re-evaluated and taking into account. This study encloses the cycle of life of a system, since diagnosis of the environment, development of the projects logical and physical, programs e implantation. Although still being tested, the release of some small surveys shows its funcionality.

This program evaluation examines the effectiveness of a school-based dental clinic. A repeated-measures design was used to longitudinally examine secondary data from participants (N = 293). Encounter intensity was developed to normalize data. Multivariate analysis of variance and Kruskal–Wallis test were used to investigate the effect of encounter intensity on the change in decay, restorations, and treatment urgency. A Pearson’s correlation was used to measure the strengths of association. Encounter intensity had a statistically significant effect on change in decay (p =.005), restorations (p =.000), and treatment urgency (p =.001). As encounter intensity increased, there was a significant association with the decrease in decay (−.167), increase in restorations (.221), and reduction in referral urgency (−.188). Incorporating dental care into a school-based health center resulted in improved oral health in underserved children while overcoming barriers that typically restrict access. The collaboration of school nurses with the school-based dental clinic was an important element for maximizing student access to dental care.

Few research studies have focused on WAC program development. Those that exist do not examine the ideological grounds for programmatic changes. This dissertation explores the dynamics of such changes through a four-year ethnographic study of WAC program development at a small, public, liberal arts college. The study employed extensive participant observation, interviewing, and document collection to trace how curricular and cultural changes around writing take shape and what ideologies and rhetorical practices come into play during that complex change process. The site for the study is of special interest because WAC there was in transition from an informal coalition focused on changing culture and pedagogy to a potentially institutional program equally invested in curricular reform. My study documents the interactions that characterize the change process, using Jenny Edbauer's conception of rhetorical ecology for its explanatory power in non-linear discursive environments. I analyze rhetorical encounters between a wide range of institutional constituents, including administrators and faculty from multiple disciplines. In these encounters, higher education's historic ideologies surface and interact in complex ways with WAC's ideologies. Using critical discourse analysis, I unpack these interactions and ideological multilectics, examining how language and values circulate among multiple users, texts, and sites within the rhetorical ecology of one college, influencing the shape of program developments. WAC scholars suggest that contemporary practitioners need to forge alliances with other cross-curricular initiatives in order for WAC to continue as a viable educational movement. My analysis of how WAC advocates at one college positioned their efforts in relation to other curricular changes reveals both benefits and costs resulting from such alliances. Although alliances can produce significant reforms, working with groups that have divergent ideological premises risks positioning WAC in subordination to others' ideological priorities. Two intertwined strategies appear to mitigate this problem: 1) ideological recentering on WAC's core theoretical commitments and 2) formation of recombinant multilectics by identifying the ideologies in play and considering how, or whether, core WAC ideological commitments align with them. Acts of recentering that incorporate deliberate multilectics may be key survival strategies for WAC programs as they interact with other cross-curricular initiatives.

In recent years, programs designed to promote financial literacy among lowincome populations have proliferated. However, such programs have largely been developed by small community-based organizations operating in isolation from one another. Most have been conducted in absence of guidance explaining how to ensure that the program meets the needs of the target audience. Very few studies have been able to link the program to subsequent increases in financial understanding or improvements in financial behaviors among participants. This thesis serves as a guidebook for community organizations that intend to provide financial literacy training to low-income audiences. The subject is introduced by offering a working definition of financial literacy, a brief overview of the state of financial literacy education in the United States, and a discussion of the importance of financial literacy. The political and social climates surrounding financial literacy are then discussed, followed by a summary of previous research studies that have found financial education to be effective. The subsequent chapters provide financial educators with practical guidance on the program's design, content, delivery, evaluation, and administration. The final chapter provides insights from the fields of economics and psychology. Supplemental resources for financial educators are found in the appendices.