Derivación deductiva de programas funcionales con patrones

Una de las dificultades principales en el desarrollo de software es la ausencia de un marco conceptual adecuado para su estudio. Una propuesta la constituye el modelo transformativo, que entiende el desarrollo de software como un proceso iterativo de transformación de especificaciones: se parte de una especificación inicial que va transformándose sucesivamente hasta obtener una especificación final que se toma como programa. Este modelo básico puede llevarse a la práctica de varias maneras. En concreto, la aproximación deductiva toma una sentencia lógica como especificación inicial y su proceso transformador consiste en la demostración de la sentencia; como producto secundario de la demostración se deriva un programa que satisface la especificación inicial. La tesis desarrolla un método deductivo para la derivación de programas funcionales con patrones, escritos en un lenguaje similar a Hope. El método utiliza una lógica multigénero, cuya relación con el lenguaje de programación es estudiada. También se identifican los esquemas de demostración necesarios para la derivación de funciones con patrones, basados en la demostración independiente de varias subsentencias. Cada subsentencia proporciona una subespecificación de una ecuación del futuro programa a derivar. Nuestro método deductivo está inspirado en uno previo de Zohar Manna y Richard Waldinger, conocido como el cuadro deductivo, que deriva programas en un lenguaje similar a Lisp. El nuevo método es una modificación del cuadro de estos autores, que incorpora géneros y permite demostrar una especificación mediante varios cuadros. Cada cuadro demuestra una subespecificación y por tanto deriva una ecuación del programa. Se prevén mecanismos para que los programas derivados puedan contener definiciones locales con patrones y variables anónimas y sinónimas y para que las funciones auxiliares derivadas no usen variables de las funciones principales. La tesis se completa con varios ejemplos de aplicación, un mecanismo que independentiza el método del lenguaje de programación y un prototipo de entorno interactivo de derivación deductiva. Categorías y descriptores de materia CR D.l.l [Técnicas de programación]: Programación funcional; D.2.10 [Ingeniería de software]: Diseño - métodos; F.3.1 [Lógica y significado de los programas]: Especificación, verificación y razonamiento sobre programas - lógica de programas; F.3.3 [Lógica y significado de los programas]: Estudios de construcciones de programas - construcciones funcionales; esquemas de programa y de recursion; 1.2.2 [Inteligencia artificial]: Programación automática - síntesis de programas; 1.2.3 [Inteligencia artificial]: Deducción y demostración de teoremas]: extracción de respuesta/razón; inducción matemática. Términos generales Programación funcional, síntesis de programas, demostración de teoremas. Otras palabras claves y expresiones Funciones con patrones, cuadro deductivo, especificación parcial, inducción estructural, teorema de descomposición.---ABSTRACT---One of the main difficulties in software development is the lack of an adequate conceptual framework of study. The transformational model is one such proposal that conceives software development as an iterative process of specifications transformation: an initial specification is developed and successively transformed until a final specification is obtained and taken as a program. This basic model can be implemented in several ways. The deductive approach takes a logical sentence as the initial specification and its proof constitutes the transformational process; as a byproduct of the proof, a program which satisfies the initial specification is derived. In the thesis, a deductive method for the derivation of Hope-like functional programs with patterns is developed. The method uses a many-sorted logic, whose relation to the programming language is studied. Also the proof schemes necessary for the derivation of functional programs with patterns, based on the independent proof of several subsentences, are identified. Each subsentence provides a subspecification of one equation of the future program to be derived. Our deductive method is inspired on a previous one by Zohar Manna and Richard Waldinger, known as the deductive tableau, which derives Lisp-like programs. The new method incorporates sorts in the tableau and allows to prove a sentence with several tableaux. Each tableau proves a subspecification and therefore derives an equation of the program. Mechanisms are included to allow the derived programs to contain local definitions with patterns and anonymous and synonymous variables; also, the derived auxiliary functions cannot reference parameters of their main functions. The thesis is completed with several application examples, i mechanism to make the method independent from the programming language and an interactive environment prototype for deductive derivation. CR categories and subject descriptors D.l.l [Programming techniques]: Functional programming; D.2.10 [Software engineering]: Design - methodologies; F.3.1 [Logics and meanings of programa]: Specifying and verifying and reasoning about programs - logics of programs; F.3.3 [Logics and meanings of programs]: Studies of program constructs - functional constructs; program and recursion schemes; 1.2.2 [Artificial intelligence]: Automatic programming - program synthesis; 1.2.3 [Artificial intelligence]: Deduction and theorem proving - answer/reason extraction; mathematical induction. General tenas Functional programming, program synthesis, theorem proving. Additional key words and phrases Functions with patterns, deductive tableau, structural induction, partial specification, descomposition theorem.

Embedding defeasible logic into logic programming

Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches. In this paper we establish close links to known semantics of logic programs. In particular, we give a translation of a defeasible theory D into a meta-program P(D). We show that under a condition of decisiveness, the defeasible consequences of D correspond exactly to the sceptical conclusions of P(D) under the stable model semantics. Without decisiveness, the result holds only in one direction (all defeasible consequences of D are included in all stable models of P(D)). If we wish a complete embedding for the general case, we need to use the Kunen semantics of P(D), instead.

Compilation by refinement for a practical assembly language

In this paper we extend the conventional framework of program refinement down to the assembler level. We describe an extension to the Refinement Calculus that supports the refinement of programs in the Guarded Command Language to programs in .NET assembler. This is illustrated by a small example.

Description and analysis of pulmonary rehabilitation care programs current state in four cities of Colombia

Purpose: there are many studies reporting the benefits of pulmonary rehabilitation, but few of them exhibit the behavior and activities of these services. This article presents the characteristics of services, parts management and training level of team members, in addition to the variables or instruments used to measure the effectiveness and impact in these programs. Method: it was made a cross sectional convenience sample which included seven pulmonary rehabilitation services in four Colombian cities (Bogotá, Medellín, Manizales and Cali), selected by the coverage, for having at least one year of experience and for being formally established and recognized nationwide. The interdisciplinary team of each service answered a survey that was validated through a pilot test and expert consensus. Participation was voluntary. Results: labor onset pulmonary rehabilitation services correspond to an average of a decade, with COPD and asthma pathologies of attention. The programs are characterized by an outpatient treatment with an average duration of eight to twelve weeks, with a frequency of an hour three times a week. Also, the director of the service is regularly a pulmonologist and the coordinator a physiotherapist (57.14%). The posgradual training of these professionals is notable, and they report to have procedural, administrative and communicative skills, but qualify regular there research skills. The physical and technological resources are well tested. 71.42% have done impact studies, but only 28.57% have been published. All have in common training in upper limbs, lower limbs, respiratory muscles, counseling, functional assessment and quality of life. The effectiveness and impact of programs is measured by the walking test, quality of life questionnaires and activities of daily living.

Migration and mobility of new Polish migrants in England:narratives of lived experience

This thesis sets out to understand the act of migrating in a period of growing movement of people. It captures the subjective experience of individual migrants, as narrated in the migration stories of 32 “new” Polish migrants in the West Midlands region of England. Since the enlargement of the European Union in 2004, over half a million Poles have arrived and registered to work in the UK, constituting one of the largest migration movements in contemporary Britain and Europe. This influx of predominantly young migrants opened up public and academic debates regarding the social relations between the Polish migrants and the host society, their duration of stay, and the impact on the economy and social services. While a substantial amount of research has now been undertaken on this migration, this thesis highlights some of the significant features of migration to Britain and Europe today, namely its dynamic, fluid, complex and varied character. Through four themes of lived experience of migration, migration and mobility, gender, and return migration, this thesis uncovers and explores the phenomenon of post-2004 EU migration from the perspective of migrants themselves. Migrant stories in this thesis are linked with experiences and meanings of migration, but also migrants’ emotions, perceptions, views and opinions. By exploring individual journeys of migration and deliberating over the determinants and consequences of migration, this thesis asks how the processes of migration and mobility come into play in the everyday lives of migrant people, and how this impacts on questions of identity, home, belonging, gender, as well as return.

Democracia Corinthiana : sentidos e significados da participação dos jogadores = Corinthians democracy : meanings and significance of the players' participation

Universidade Estadual de Campinas . Faculdade de Educação Física

Influence of Firms’ Environmental Management and Community Involvement Programs in their Employees and in the Community

To assure enduring success, firms need to generate economic value with respect for the environment and social value. They also need to be aware of the needs and expectations of relevant stakeholders and incorporate them in their business strategies and programs. These challenges imply that engineers should take into consideration societal, health and safety,environmental and commercial issues in their professional activity. This investigation accesses the influence of firms’ environmental management programs and community involvement programs on their own employees and in the community, with a focus on small and medium companies. Based on a quantitative research, the findings suggest that firms that invest both in environmental management programs and in community involvement programs have a higher involvement of their own employees with the community, while at the same time receiving more feedback (positive, but also negative) from the community, stressing the need to pay special attention to their communication policies.

Objectives of social entrepreneurs and federal lending programs, and the optimal allocation of external funds

Magdeburg, Univ., Fak. für Wirtschaftswiss., Diss., 2010

Inventory and description of disease management programs in Switzerland

Background: Disease management, a system of coordinated health care interventions for populations with chronic diseases in which patient self-care is a key aspect, has been shown to be effective for several conditions. Little is known on the supply of disease management programs in Switzerland. Objectives: To systematically search, record and evaluate data on existing disease management programs in Switzerland. Methods: Programs met our operational definition of disease management if their interventions targeted a chronic disease, included a multidisciplinary team and lasted at least 6 months. To find existing programs, we searched Swiss official websites, Swiss web-pages using Google, medical electronic database (Medline), and checked references from selected documents. We also contacted personally known individuals, those identified as possibly working in the field, individuals working in major Swiss health insurance companies and people recommended by previously contacted persons (snow ball strategy). We developed an extraction grid and collected information pertaining to the following 8 domains: patient population, intervention recipient, intervention content, delivery personnel, method of communication, intensity and complexity, environment and clinical outcomes (measures?). Results: We identified 8 programs fulfilling our operational definition of disease management. Programs targeted patients with diabetes, hypertension, heart failure, obesity, alcohol dependence, psychiatric disorders or breast cancer, and were mainly directed towards patients. The interventions were multifaceted and included education in almost all cases. Half of the programs included regularly scheduled follow-up, by phone in 3 instances. Healthcare professionals involved were physicians, nurses, case managers, social workers, psychologists and dietitians. None fulfilled the 6 criteria established by the Disease Management Association of America. Conclusions: Our study shows that disease management programs, in a country with universal health insurance coverage and little incentive to develop new healthcare strategies, are scarce, although we may have missed existing programs. Nonetheless, those already implemented are very interesting and rather comprehensive. Appropriate evaluation of these programs should be performed in order to build upon them and try to design a generic disease management framework suited to the Swiss healthcare system.

Inventory and perspectives of chronic disease management programs in Switzerland: an exploratory survey.

OBJECTIVE: To describe chronic disease management programs active in Switzerland in 2007, using an exploratory survey. METHODS: We searched the internet (Swiss official websites and Swiss web-pages, using Google), a medical electronic database (Medline), reference lists of pertinent articles, and contacted key informants. Programs met our operational definition of chronic disease management if their interventions targeted a chronic disease, included a multidisciplinary team (>/=2 healthcare professionals), lasted at least six months, and had already been implemented and were active in December 2007. We developed an extraction grid and collected data pertaining to eight domains (patient population, intervention recipient, intervention content, delivery personnel, method of communication, intensity and complexity, environment, clinical outcomes). RESULTS: We identified seven programs fulfilling our operational definition of chronic disease management. Programs targeted patients with diabetes, hypertension, heart failure, obesity, psychosis and breast cancer. Interventions were multifaceted; all included education and half considered planned follow-ups. The recipients of the interventions were patients, and healthcare professionals involved were physicians, nurses, social workers, psychologists and case managers of various backgrounds. CONCLUSIONS: In Switzerland, a country with universal healthcare insurance coverage and little incentive to develop new healthcare strategies, chronic disease management programs are scarce. For future developments, appropriate evaluations of existing programs, involvement of all healthcare stakeholders, strong leadership and political will are, at least, desirable.

Characteristics and effectiveness of diabetes self-management educational programs targeted to racial/ethnic minority groups: a systematic review, meta-analysis and meta-regression.

BACKGROUND It is not clear to what extent educational programs aimed at promoting diabetes self-management in ethnic minority groups are effective. The aim of this work was to systematically review the effectiveness of educational programs to promote the self-management of racial/ethnic minority groups with type 2 diabetes, and to identify programs' characteristics associated with greater success. METHODS We undertook a systematic literature review. Specific searches were designed and implemented for Medline, EMBASE, CINAHL, ISI Web of Knowledge, Scirus, Current Contents and nine additional sources (from inception to October 2012). We included experimental and quasi-experimental studies assessing the impact of educational programs targeted to racial/ethnic minority groups with type 2 diabetes. We only included interventions conducted in countries members of the OECD. Two reviewers independently screened citations. Structured forms were used to extract information on intervention characteristics, effectiveness, and cost-effectiveness. When possible, we conducted random-effects meta-analyses using standardized mean differences to obtain aggregate estimates of effect size with 95% confidence intervals. Two reviewers independently extracted all the information and critically appraised the studies. RESULTS We identified thirty-seven studies reporting on thirty-nine educational programs. Most of them were conducted in the US, with African American or Latino participants. Most programs obtained some benefits over standard care in improving diabetes knowledge, self-management behaviors and clinical outcomes. A meta-analysis of 20 randomized controlled trials (3,094 patients) indicated that the programs produced a reduction in glycated hemoglobin of -0.31% (95% CI -0.48% to -0.14%). Diabetes knowledge and self-management measures were too heterogeneous to pool. Meta-regressions showed larger reduction in glycated hemoglobin in individual and face to face delivered interventions, as well as in those involving peer educators, including cognitive reframing techniques, and a lower number of teaching methods. The long-term effects remain unknown and cost-effectiveness was rarely estimated. CONCLUSIONS Diabetes self-management educational programs targeted to racial/ethnic minority groups can produce a positive effect on diabetes knowledge and on self-management behavior, ultimately improving glycemic control. Future programs should take into account the key characteristics identified in this review.