A partial-correctness semantics for modelling assembler programs

Previous work on formally modelling and analysing program compilation has shown the need for a simple and expressive semantics for assembler level programs. Assembler programs contain unstructured jumps and previous formalisms have modelled these by using continuations, or by embedding the program in an explicit emulator. We propose a simpler approach, which uses techniques from compiler theory in a formal setting. This approach is based on an interpretation of programs as collections of program paths, each of which has a weakest liberal precondition semantics. We then demonstrate, by example, how we can use this formalism to justify the compilation of block-structured high-level language programs into assembler.

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.

Primary classroom teachers' use of social and emotional wellbeing programs and the factors influencing program use

There has been a rapid escalation in the development and evaluation of social and emotional well-being (SEW) programs in primary schools over the last few decades. Despite the plethora of programs available, primary teachers’ use of SEW programs is not well documented in Australian schools, with even less consideration of the factors influencing program use. A cross-sectional survey was undertaken with primary classroom teachers across twelve schools in the Brisbane and Sunshine Coast Education Districts in Queensland, Australia, during 2005. A checklist of SEW programs and an audit of SEW practices in schools were employed to investigate the number, range and types of SEW programs used by primary classroom teachers and the contextual factors influencing program use. Whilst the majority of implementation studies have been conducted under intervention conditions, this study was designed to capture primary classroom teachers’ day-to-day use of SEW programs and the factors influencing program use under real-world conditions. The findings of this research indicate that almost three quarters of the primary classroom teachers involved in the study reported using at least one SEW program during 2005. Wide variation in the number and range of programs used was evident, suggesting that teachers are autonomous in their use of SEW programs. Evidence-based SEW programs were used by a similar proportion of teachers to non-evidence-based programs. However, irrespective of the type of program used, primary teachers overwhelmingly reported using part of a SEW program rather than the whole program. This raises some issues about the quality of teachers’ program implementation in real-world practice, especially with respect to programs that are evidence-based. A content analysis revealed that a wide range of factors have been examined as potential influences on teachers’ implementation of health promotion programs in schools, including SEW programs, despite the limited number of studies undertaken to date. However, variation in the factors examined and study designs employed both within and across health promotion fields limited the extent to which studies could be compared. A methodological and statistical review also revealed substantial variation in the quality of reporting of studies. A variety of factors were examined as potential influences on primary classroom teachers’ use of SEW programs across multiple social-ecological levels of influence (ranging from community to school and individual levels). In this study, parent or caregiver involvement in class activities and the availability of wellbeing-related policies in primary schools were found to be influential in primary classroom teachers’ use of SEW programs. Teachers who often or always involve parents or caregivers in class activities were at a higher odds of program use relative to teachers who never or rarely involved parents or caregivers in class activities. However, teachers employed in schools with the highest number of wellbeing-related policies available were at a lower odds of program use relative to teachers employed in schools with fewer wellbeing-related policies available. Future research should investigate primary classroom teachers’ autonomy and motivations for using SEW programs and the reasons behind the selection and use of particular types of programs. A larger emphasis should also be placed upon teachers not using SEW programs to identify valid reasons for non-use. This would provide another step towards bridging the gap between the expectations of program developers and the needs of teachers who implement programs in practice. Additionally, the availability of wellbeing-related school policies and the types of activities that parents and caregivers are involved with in the classroom warrant more in-depth investigation. This will help to ascertain how and why these factors influence primary classroom teachers’ use of SEW programs on a day-to-day basis in schools.

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.

Learning approach and perception of learning context in economics education : a causality test

In the study of student learning literature, the traditional view holds that when students are faced with heavy workload, poor teaching, and content that they cannot relate to – important aspects of the learning context, they will more likely utilise the surface approach to learning due to stresses, lack of understanding and lack of perceived relevance of the content (Kreber, 2003; Lizzio, Wilson, & Simons, 2002; Ramdsen, 1989; Ramsden, 1992; Trigwell & Prosser, 1991; Vermunt, 2005). For example, in studies involving health and medical sciences students, courses that utilised student-centred, problem-based approaches to teaching and learning were found to elicit a deeper approach to learning than the teacher-centred, transmissive approach (Patel, Groen, & Norman, 1991; Sadlo & Richardson, 2003). It is generally accepted that the line of causation runs from the learning context (or rather students’ self reported data on the learning context) to students’ learning approaches. That is, it is the learning context as revealed by students’ self-reported data that elicit the associated learning behaviour. However, other research studies also found that the same teaching and learning environment can be perceived differently by different students. In a study of students’ perceptions of assessment requirements, Sambell and McDowell (1998) found that students “are active in the reconstruction of the messages and meanings of assessment” (p. 391), and their interpretations are greatly influenced by their past experiences and motivations. In a qualitative study of Hong Kong tertiary students, Kember (2004) found that students using the surface learning approach reported heavier workload than students using the deep learning approach. According to Kember if students learn by extracting meanings from the content and making connections, they will more likely see the higher order intentions embodied in the content and the high cognitive abilities being assessed. On the other hand, if they rote-learn for the graded task, they fail to see the hierarchical relationship in the content and to connect the information. These rote-learners will tend to see the assessment as requiring memorising and regurgitation of a large amount of unconnected knowledge, which explains why they experience a high workload. Kember (2004) thus postulate that it is the learning approach that influences how students perceive workload. Campbell and her colleagues made a similar observation in their interview study of secondary students’ perceptions of teaching in the same classroom (Campbell et al., 2001). The above discussions suggest that students’ learning approaches can influence their perceptions of assessment demands and other aspects of the learning context such as relevance of content and teaching effectiveness. In other words, perceptions of elements in the teaching and learning context are endogenously determined. This study attempted to investigate the causal relationships at the individual level between learning approaches and perceptions of the learning context in economics education. In this study, students’ learning approaches and their perceptions of the learning context were measured. The elements of the learning context investigated include: teaching effectiveness, workload and content. The authors are aware of existence of other elements of the learning context, such as generic skills, goal clarity and career preparation. These aspects, however, were not within the scope of this present study and were therefore not investigated.

Experiences and desires of people with tetraplegia living with and without electronic aids to daily living: an Irish focus group study

This qualitative descriptive study explores the lived experience for persons with a high cervical spinal cord injury who have Electronic Aids to Daily Living (EADLs), and for persons who have no EADLs. Fifteen people with cervical spinal cord injuries attended four focus groups. Data analysis uncovered a novel framework of several themes that were organised into three categories: experiences, desires and meanings of living with EADL. Users’ and non users’ groups revealed homogenous themes. Experiences and desires are explored further in this paper. Themes within the category of experiences included: EADL devices, supply support and training, abandonment, mouthsticks and powered wheelchairs. Desires included: simple stuff, reliability, aesthetics and voice activation. Findings offer valuable personal insights about life with EADL to be considered by all involved with EADL.

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.

Where money and meanings meet : theorizing the emergence of new values in media and education

Recent developments in technology, globalization, and consumer activism have challenged the "broadcasting model" of natonally bounded, vertically integrated, monopolistic, expert-paradigm media industries, dedicated to supplying leisure entertainment to more or less passive consumers. Instead, attention has turned to globally traded formats, social network markets, consumer-created content, multiplatform "publication," and a semiotic long tail where niche representations can be as valuable as blockbusters. Such chenges are just as much a challenge to education as they are to business models. And education, both formal and informal, is a dynamic agent in these processes, participation, and creative content require a rethink of "studies" just as much as of "media."