Supporting contexts in program refinement

A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the program. However, refinement of a component can depend on the context of the component for information about the variables that are in scope and what their types are. The refinement can also take advantage of additional information, such as any precondition the component can assume. The aim of this paper is to introduce a technique, which we call program window inference, to handle such contextual information during derivations in the refinement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize refinement using program window inference. (C) 1997 Elsevier Science B.V.

The variety of variables in automated real-time refinement

The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.

Restaurant Health and Hygiene: A Model Program with Theory-Based Guidelines for Implementation

Poor hygienic practices and illness of restaurant employees are major contributors to the contamination of food and the occurrence of food-borne illness in the United States, costing the food industry and society billions of dollars each year. Risk factors associated with this problem include lack of proper handwashing; food handlers reporting to work sick; poor personal hygiene; and bare hand contact with ready-to-eat foods. However, traditional efforts to control these causes of food-borne illness by public health authorities have had limited impact, and have revealed the need for comprehensive and innovative programs that provide active managerial control over employee health and hygiene in restaurant establishments. Further, the introduction and eventual adoption by the food industry of such programs can be facilitated through the use of behavior-change theory. This Capstone Project develops a model program to assist restaurant owners and operators in exerting active control over health and hygiene in their establishments and provides theory-based recommendations for the introduction of the program to the food industry.

Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

A technique for modular logic program refinement

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we introduce modules into a logic programming refinement calculus. Modules allow data types to be grouped together with sets of procedures that manipulate the data types. By placing restrictions on the way a program uses a module, we develop a technique for refining the module so that it uses a more efficient representation of the data type.

Procedure compilation in the refinement calculus

High-level language program compilation strategies can be proven correct by modelling the process as a series of refinement steps from source code to a machine-level description. We show how this can be done for programs containing recursively-defined procedures in the well-established predicate transformer semantics for refinement. To do so the formalism is extended with an abstraction of the way stack frames are created at run time for procedure parameters and variables.

Refinement laws for verifying library subroutine adaptation

In component-based software engineering programs are constructed from pre-defined software library modules. However, if the library's subroutines do not exactly match the programmer's requirements, the subroutines' code must be adapted accordingly. For this process to be acceptable in safety or mission-critical applications, where all code must be proven correct, it must be possible to verify the correctness of the adaptations themselves. In this paper we show how refinement theory can be used to model typical adaptation steps and to define the conditions that must be proven to verify that a library subroutine has been adapted correctly.

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.

Making Life Choices Program: A psychoeducational intervention for promoting critical cognitive and affective competencies in adolescents at-risk for problem behaviors

The long term goal of the work described is to contribute to the emerging literature of prevention science in general, and to school-based psychoeducational interventions in particular. The psychoeducational intervention reported in this study used a main effects prevention intervention model. The current study focused on promoting optimal cognitive and affective functioning. The goal of this intervention was to increase potential protective factors such as critical cognitive and communicative competencies (e.g., critical problem solving and decision making) and affective competencies (e.g., personal control and responsibility) in middle adolescents who have been identified by the school system as being at-risk for problem behaviors. The current psychoeducational intervention draws on an ongoing program of theory and research (Berman, Berman, Cass Lorente, Ferrer Wreder, Arrufat, & Kurtines 1996; Ferrer Wreder, 1996; Kurtines, Berman, Ittel, & Williamson, 1995) and extends it to include Freire's (1970) concept of transformative pedagogy in developing school-based psychoeducational programs that target troubled adolescents. The results of the quantitative and qualitative analyses indicated trends that were generally encouraging with respect to the effects of the intervention on increasing critical cognitive and affective competencies. ^

"Family Education and Support" program for families at psychosocial risk: the role of implementation process

This paper analyses the implementation characteristics of the Family Education and Support program, a theory-driven, needs-based, and evidence-based positive parenting program originally developed for the Andalusian family preservation services. The implementation process of 34 trials of the FAF program with 155 participants was analyzed. Cluster analyses were also performed to explore variability in implementation conditions from a comprehensive perspective. Results showed different implementation profiles that moderated the FAF effectiveness (namely lengthier interventions, higher program fidelity, and practitioners' positive perceptions and satisfaction with the program). The relevance of examining implementation process across several trials is discussed in order to distinguish core and non-core FAF components, as well as the need for combining faithful and adaptable implementations that guarantee the ecologic validity of evidence-based positive parenting programs.

Emoções positivas e motivação na reabilitação biopsicossocial

RESUMO: O presente estudo tem como principal objectivo verificar o fluxo emocional e a motivação para a mudança num programa de reabilitação biopsicossocial de alcoolismo e toxicodependências, com a duração de quatro semanas. Para esse efeito, procedeu-se à recolha da amostra de 30 participantes dentro do programa, utilizando para avaliar o fluxo emocional os relatos de episódios emocionais, o Teste de Positividade (TP), a Analogical Emotional Scale (AES), o Subjective Well-being (SWB), o Controlo Percebido Subjectivo (CPS) em três momentos distintos do programa, pelo que para avaliar a motivação foi utilizada a escala SOCRATES 8D no inicio e no final do programa de reabilitação. A teoria argumenta a existência de um aumento na satisfação pessoal e nas emoções positivas durante o processo de mudança, ou seja, quando o processo terapêutico decorre de forma favorável. Os resultados confirmam a existência de uma evolução linear positiva no TP, como também no SWB e CPS. Contudo não foi totalmente confirmado um aumento positivo da motivação, pelo que os resultados apenas demonstraram diferenças significativas na subescala Ambivalência da escala SOCRATES 8D, verificando-se um decréscimo acentuado entre os dois momentos, o que se revela favorável para o processo de mudança desejado no programa. ABSTRACT: The main objective of this study is to verify the emotional flow and the motivation for change process in a bio-psychosocial rehabilitation program for alcoholism and drug addictions, with a duration of four weeks. To this end, we proceeded to collect the sample of 30 participants in the program, to evaluate the emotional flow we use the emotional reports, the Positivity Test (PT), the Analogical Emotional Scale (AES), the Subjective Well-Being (SWB), the Subjective Perceived Control (PSC) in three separate moments of the program, to assess the motivation scale was used the SOCRATES 8D scale at the beginning and in the end of the rehabilitation program. The theory argues that there is an increase in personal satisfaction and positive emotions during the change process, when the therapeutic process runs optimally. The results confirm the existence of a positive linear trend in the PT, in SWB and CPS. However it was not totally confirmed an positive increase in motivation, so the results only showed significant differences in ambivalence subscale of the SOCRATES 8D, and there is a sharp decrease between the two moments, which proves favorable for the desired process of change in the program.

Fitness, inclusive fitness, and optimization

Individual-as-maximizing agent analogies result in a simple understanding of the functioning of the biological world. Identifying the conditions under which individuals can be regarded as fitness maximizing agents is thus of considerable interest to biologists. Here, we compare different concepts of fitness maximization, and discuss within a single framework the relationship between Hamilton's (J Theor Biol 7: 1-16, 1964) model of social interactions, Grafen's (J Evol Biol 20: 1243-1254, 2007a) formal Darwinism project, and the idea of evolutionary stable strategies. We distinguish cases where phenotypic effects are additive separable or not, the latter not being covered by Grafen's analysis. In both cases it is possible to define a maximand, in the form of an objective function phi(z), whose argument is the phenotype of an individual and whose derivative is proportional to Hamilton's inclusive fitness effect. However, this maximand can be identified with the expression for fecundity or fitness only in the case of additive separable phenotypic effects, making individual-as-maximizing agent analogies unattractive (although formally correct) under general situations of social interactions. We also feel that there is an inconsistency in Grafen's characterization of the solution of his maximization program by use of inclusive fitness arguments. His results are in conflict with those on evolutionary stable strategies obtained by applying inclusive fitness theory, and can be repaired only by changing the definition of the problem.

Reliability of a quantitative clinical posture assessment tool among persons with idiopathic scoliosis

Objective To determine overall, test–retest and inter-rater reliability of posture indices among persons with idiopathic scoliosis. Design A reliability study using two raters and two test sessions. Setting Tertiary care paediatric centre. Participants Seventy participants aged between 10 and 20 years with different types of idiopathic scoliosis (Cobb angle 15 to 60°) were recruited from the scoliosis clinic. Main outcome measures Based on the XY co-ordinates of natural reference points (e.g. eyes) as well as markers placed on several anatomical landmarks, 32 angular and linear posture indices taken from digital photographs in the standing position were calculated from a specially developed software program. Generalisability theory served to estimate the reliability and standard error of measurement (SEM) for the overall, test–retest and inter-rater designs. Bland and Altman's method was also used to document agreement between sessions and raters. Results In the random design, dependability coefficients demonstrated a moderate level of reliability for six posture indices (ϕ = 0.51 to 0.72) and a good level of reliability for 26 posture indices out of 32 (ϕ ≥ 0.79). Error attributable to marker placement was negligible for most indices. Limits of agreement and SEM values were larger for shoulder protraction, trunk list, Q angle, cervical lordosis and scoliosis angles. The most reproducible indices were waist angles and knee valgus and varus. Conclusions Posture can be assessed in a global fashion from photographs in persons with idiopathic scoliosis. Despite the good reliability of marker placement, other studies are needed to minimise measurement errors in order to provide a suitable tool for monitoring change in posture over time.

Redução de custo na manutenção de ativos no Ambiente Industrial

Pós-graduação em Engenharia de Produção - FEG