bluuebunny/crossref_metadata_2025_split huggingface dataset:
Object-extending class transformations
Authors: Lieberherr Karl J. , Hürsch Walter L. , Xiao Cun 
Published: February 2005

Abstract
Reorganisation and evolution of class hierarchies is important for object-oriented system development and has received considerable attention in the literature. The contributions of this paper are: (1) a formal study of a set of extension relations and transformations on class hierarchies; (2) a presentation of a small set of primitive transformations which form a minimal and complete basis for the extension relations; and (3) an analysis of the impact of these transformations at the object level.

The study leads to a better understanding of evolution and reuse of object-oriented software and class hierarchies. It also provides a terminology and a means of classification for design reuse. The theory presented in this paper is based on the Demeter data model, which gives a concise mathematical foundation for classes and their inheritance and part-of relationships. Parts of the theory have been implemented in the Demeter System

TM

C++, a CASE tool for object-oriented design and programming.
List partitions
Authors: Bird R. S. , de Moor O. 
Published: February 2005

Abstract

By definition, a
partition
of a list is a division of that list into nonempty contiguous segments. Many programming and operations research problems can be specified in terms of list partitions, and we present a hierarchy of theorems for deriving programs from such specifications. Throughout, reasoning is conducted in an equational style using the calculus for program synthesis developed by Bird and Meertens.
Types with intersection: An introduction
Authors: Hindley J. Roger 
Published: February 2005

Abstract

This paper is an informal introduction to the theory of types which use a connective “∧” for the intersection of two types and a constant “
ω
” for a universal type, besides the usual connective “→” for function-types. This theory was first devised in about 1977 by Coppo, Dezani and Sallé in the context of
λ
-calculus and its main development has been by Coppo and Dezani and their collaborators in Turin. With suitable axioms and rules to assign types to
λ
-calculus terms, they obtained a system in which (i) the set of types given to a term does not change under
λ
-conversion, (ii) some interesting sets of terms, for example the solvable terms and the terms with normal form, can be characterised exactly by the types of their members, and (iii) the type-apparatus is not so complex as polymorphic systems with quantifier-containing types and therefore probably not so expensive to implement mechanically as these systems.

There are in fact several variant systems with different detailed properties. This paper defines and motivates the simplest one from which the others are derived, and describes its most basic properties. No proofs are given but the motivation is shown by examples. A comprehensive bibliography is included.
Towards a formal foundation of the specification and description language SDL
Authors: Broy Manfred 
Published: February 2005

Abstract
A formal model is described for the CCITT specification and description language SDL which provides a graphical concept for representing designs of systems interacting by signals. The model is based on functional descriptions of interactive systems using the concept of streams and stream processing functions. The foundations for this functional modelling of interactive systems are introduced. The graphical constructs of SDL are related to this model. In particular it is shown how the meaning of SDL graphical forms can be represented by specifications in the form of conditional equations or by functional programs. Based on the functional formal model the application of specification and verification methods for SDL is demonstrated. Small examples are treated. A number of tools are discussed that can be based on that model.
This study does not define a semantic model for the specification and design language SDL, but it gives
An introduction to the functional modelling of distributed systems
An explanation of how to translate SDL designs into functional descriptions An extended example for the translation of an SDL design
A discussion of the possibilities of supporting SDL designs by such a semantic foundation
Structured calculational proof
Authors: Back Ralph , Grundy Jim , von Wright Joakim 
Published: February 2005

Abstract

We propose a new format for writing proofs, called
structured calculational proof
. The format resembles the calculational style already familiar to many computer scientists, but extends it to allow the hierarchical decomposition of larger proofs into smaller ones. Structured calculation is actually an alternative presentation of natural deduction, a style of reasoning which uses hierarchical decomposition to great effect, but which is traditionally expressed in a notation that is inconvenient for writing calculational proofs. The hierarchical nature of structured calculational proofs can be used for browsing proofs in electronic publications.
An algebraic verification of a mobile network
Authors: Orava Fredrik , Parrow Joachim 
Published: February 2005

Abstract

In a mobile communication network some nodes change locations, and are therefore connected to different other nodes at different points in time. We show how some important aspects of such a network can be formally defined and verified using the
π
-calculus, which is a development of CCS (Calculus of Communicating Systems) allowing port names to be sent as parameters in communication events. As an example of a mobile network we consider the Public Land Mobile Network currently being developed by the European Telecommunication Standards Institute and concentrate on the handover procedure which controls the dynamic topology of the network.
On equivalence-completions of fairness assumptions
Authors: Francez Nissim , Back Ralph -J. J. , Kurki-Suonio Reino 
Published: February 2005

Abstract

The paper considers the treatment of fairness assumptions which are
not equivalence-robust
, a central issue in relating
interleaving semantics
to
partial order semantics
. A notion of
completion
is introduced and studied, and two specific completions are considered:
maximal completion
, which is easier to implement (shown by a broadcast bus implementation) but guarantees only weak liveness properties of programs using it; and
minimal completion
, which may be harder to implement but induces stronger liveness properties on programs using it. Some properties of completions are formulated. Finally, the impact of non-equivalence-robustness on compositionality with respect to separate fairness assumptions is considered.
TIC: A timed calculus
Authors: Quemada Juan , de Frutos David , Azcorra Arturo 
Published: February 2005

Abstract
TIC is a timed algebraic calculus which combines ideas from asynchronous and synchronous calculi. Time is introduced by assigning explicit time restrictions to the events of an asynchronous calculus. The semantics is defined in an operational way. Interleaving of behaviours is defined in such a way that a proper merge of events in time is achieved. Weak timed bisimulation is also defined. Examples are presented to show the applicability of the calculus to the study of timed behaviours.
Proof by analogy in mural
Authors: Vadera Sunil 
Published: February 2005

Abstract
An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct?
One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming.
This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.
Interpreting Message Flow Graphs
Authors: Ladkin Peter B. , Leue Stefan 
Published: February 2005

Abstract
We give a semantics for Message Flow Graphs (MFGs), which play the role for interprocess communication that Program Dependence Graphs play for control flow in parallel processes. MFGs have been used to analyse parallel code, and are closely related to Message Sequence Charts and Time Sequence Diagrams in telecommunications systems. Our requirements are firstly, to determine unambiguously exactly what execution traces are specified by an MFG, and secondly, to use a finite-state interpretation. Our methods function for both asynchronous and synchronous communications. From a set of MFGs, we define a transition system of global states, and from that a Büchi automaton by considering safety and liveness properties of the system. In order easily to describe liveness properties, we interpret the traces of the transition system as a model of Manna-Pnueli temporal logic. Finally, we describe the expressive power of MFGs by mimicking an arbitrary Büchi automaton by means of a set of MFGs.
Safety, liveness and fairness in temporal logic
Authors: Sistla A. Prasad 
Published: February 2005

Abstract
In this paper we present syntactic characterization of temporal formulas that express various properties of interest in the verification of concurrent programs. Such a characterization helps us in choosing the right techniques for proving correctness with respect to these properties. The properties that we consider include safety properties, liveness properties and fairness properties. We also present algorithms for checking if a given temporal formula expresses any of these properties.
Processes with probabilities, priority and time
Authors: Tofts Chris 
Published: February 2005

Abstract
A probabilistic calculus, derived from Milner's SCCS, WSCCS is presented. We define a notion of bisimulation for probabilistic processes and show that it is a congruence. A simple equational characterisation is shown to be both sound and complete for finite processes. We present many examples including some extended ones. The larger examples show both the expressive power of WSCCS and the availability of simple proof methods for some complex systems.
Temporal theories as modularisation units for concurrent system specification
Authors: Fiadeiro J. , Maibaum T. 
Published: February 2005

Abstract
In this paper, we bring together the use of temporal logic for specifying concurrent systems, in the tradition initiated by A. Pnueli, and the use of tools from category theory as a means for structuring specifications as combinations of theories in the style developed by R. Burstall and J. Goguen. As a result, we obtain a framework in which systems of interconnected components can be described by assembling the specifications of their components around a diagram, using theory morphisms to specify how the components interact. This view of temporal theories as specification units naturally brings modularity to the description and analysis of systems. Moreover, it becomes possible to import into the area of formal development of reactive systems the wide body of specification techniques that have been defined for structuring specifications independently of the underlying logic, and that have been applied with great success in the area of Abstract Data Types. Finally, as a discipline of design, we use the object-oriented paradigm according to which components keep private data and interact by sharing actions, with a view towards providing formal tools for the specification of concurrent objects.
Discrete time process algebra
Authors: Baeten J. C. M. , Bergstra J. A. 
Published: February 2005

Abstract
The axiom system ACP of [BeK84a] was extended with real time features in [BaB91]. Here we proceed to define a discrete time extension of ACP, along the lines of ATP [NiS94]. We present versions based on relative timing and on absolute timing. Both approaches are integrated using parametric timing. The time free ACP theory is embedded in the discrete time theory.
Hoare's logic and VDM
Authors: Coenen J. 
Published: February 2005

Abstract
A relational framework which unifies Hoare's logic and VDM is presented. Within this framework a partial correctness version of VDM is defined. It is argued that this partial correctness version of VDM is intuitive and consistent with the original total correctness version. Furthermore it is shown how both partial and total correctness formulae and specifications can be translated from Hoare's logic into VDM and vice versa. VDM's satisfiability requirement is briefly discussed, and a similar condition for Hoare's logic is defined.:
The consistency theorem for free type definitions in Z
Authors: Spivey Michael 
Published: February 2005

Abstract

Successive editions of the author's reference manual for the Z specification language [ZRM89, ZRM92] gave different sufficient conditions for the consistency of free type definitions. Both were expressed in terms of the settheoretic constructions present in the type definition. Whilst the first edition specified that these constructions should be
continuous
, in the sense that they preserve limits of ascending chains of sets, the second edition specified that they should be
finitary
, i.e., that the result of each construction should be the union of a set of finite approximations. This short note clarifies the relationship between these two conditions.
Modular structuring of VDM specifications in VVSL
Authors: Middelburg C. A. 
Published: February 2005

Abstract

VVSL is a language for writing modularly structured VDM specifications. Its modularisation mechanism permits two modules to have parts of their state in common, including hidden parts. Firstly, this paper gives an overview of the structuring sublanguage of VVSL and a concise description of its semantic foundations: DA (a general algebraic model of modules) and
λπ
-calculus (a variant of classical lambda calculus). The paper also presents a variation on a “challenge problem” of Fitzgerald and Jones as an example of the use of VVSL's structuring language. Finally, their modular structuring style and the suggested language features to support it are commented upon.
When is partial trace equivalence adequate?
Authors: Bloom Bard 
Published: February 2005

AbstractTwo processes arepartial trace equivalentiff they can perform the same sequences of actions in isolation. Partial trace equivalence is perhaps the simplest possible notion of process equivalence. In general, it is too simple: it is not usually an adequate semantics. We investigate the circumstances under which it is adequate, which are surprisingly rich. We give two substantial classes of languages for which partial traces are adequate. In one class, partial trace equivalence suffices for total correctness, and operations such as true sequencing are possible; but all processes are determinate and silent moves are not possible. The other class — which includes many standard process calculi, such as CCS and CSP — admits indeterminacy and silent moves, but partial traces only suffice for partial correctness and true sequencing is not definable.
A theory of processes with localities
Authors: Boudol G. , Castellani I. , Hennessy M. , Kiehn A. 
Published: February 2005

AbstractWe study a notion of observation for concurrent processes which allows the observer to see the distributed nature of processes, giving explicit names for the location of actions. A general notion of bisimulation related to this observation of distributed systems is introduced. Our main result is that these bisimulation relations, particularized to a process algebra extending CCS, are completely axiomatizable. We discuss in detail two instances of location bisimulations, namely the location equivalence and the location preorder.
Image, context and transition: smoking in mid‐to‐late adolescence
Authors: Wiltshire Susan , Amos Amanda , Haw Sally , McNeill Ann 
Published: February 2005

ABSTRACTThis paper explores 16–19‐year‐old Scottish smokers’ experiences and attitudes towards smoking and their understandings of the ways in which this transitional period impacts on their smoking behaviour. The study involved 49 qualitative interviews conducted mostly in friendship pairs. Interviewees also completed a brief smoking questionnaire. The paper highlights the salience of social context in smoking initiation and maintenance, and the role of smoking across a range of social spheres. Interviewees described how transitions from school to work, further education or un/employment, impacted on their smoking. Smoking was perceived to be an important ‘lubricant’ for social relations, and marker of an acceptable identity in familiar and new contexts which acted to reinforce and increase smoking. In contrast, smoking restrictions at home, work and/or educational settings were felt to moderate consumption. This has implications for cessation programmes for older adolescents who have been relatively ignored by tobacco control. The study also suggests that if smoke‐free policies were extended to all workplaces, this would have a particular impact on smoking amongst older adolescents by hindering the transition from social to regular smoking.
Using evolutionary Expectation Maximization to estimate indel rates
Authors: Holmes Ian 
Published: February 2005

AbstractMotivationThe Expectation Maximization (EM) algorithm, in the form of the Baum–Welch algorithm (for hidden Markov models) or the Inside-Outside algorithm (for stochastic context-free grammars), is a powerful way to estimate the parameters of stochastic grammars for biological sequence analysis. To use this algorithm for multiple-sequence evolutionary modelling, it would be useful to apply the EM algorithm to estimate not only the probability parameters of the stochastic grammar, but also the instantaneous mutation rates of the underlying evolutionary model (to facilitate the development of stochastic grammars based on phylogenetic trees, also known as Statistical Alignment). Recently, we showed how to do this for the point substitution component of the evolutionary process; here, we extend these results to the indel process.ResultsWe present an algorithm for maximum-likelihood estimation of insertion and deletion rates from multiple sequence alignments, using EM, under the single-residue indel model owing to Thorne, Kishino and Felsenstein (the ‘TKF91’ model). The algorithm converges extremely rapidly, gives accurate results on simulated data that are an improvement over parsimonious estimates (which are shown to underestimate the true indel rate), and gives plausible results on experimental data (coronavirus envelope domains). Owing to the algorithm's close similarity to the Baum–Welch algorithm for training hidden Markov models, it can be used in an ‘unsupervised’ fashion to estimate rates for unaligned sequences, or estimate several sets of rates for sequences with heterogenous rates.AvailabilitySoftware implementing the algorithm and the benchmark is available under GPL from http://www.biowiki.org/Contactihh@berkeley.edu
Recovery from DSM‐IV alcohol dependence: United States, 2001–2002
Authors: Dawson Deborah A. , Grant Bridget F. , Stinson Frederick S. , Chou Patricia S. , Huang Boji , Ruan W. June 
Published: February 2005

ABSTRACTAims  To investigate the prevalence and correlates of recovery from Diagnostic and Statistical Manual version IV (DSM‐IV) alcohol dependence by examining the past‐year status of individuals who met the criteria for prior‐to‐past‐year (PPY) dependence.Design  Cross‐sectional, retrospective survey of a nationally representative sample of US adults 18 years of age and over (first wave of a planned longitudinal survey).Methods  This analysis is based on data from the 2001–02 National Epidemiologic Survey on Alcohol and Related Conditions (NESARC), in which data were collected in personal interviews conducted with one randomly selected adult in each sample household. A subset of the NESARC sample (total n = 43 093), consisting of 4422 US adults 18 years of age and over classified with PPY DSM‐IV alcohol dependence, were evaluated with respect to their past‐year recovery status: past‐year dependence, partial remission, full remission, asymptomatic risk drinking, abstinent recovery (AR) and non‐abstinent recovery (NR). Correlates of past‐year status were examined in bivariate analyses and using multivariate logistic regression models.Findings  Of people classified with PPY alcohol dependence, 25.0% were still classified as dependent in the past year; 27.3% were classified as being in partial remission; 11.8% were asymptomatic risk drinkers who demonstrated a pattern of drinking that put them at risk of relapse; 17.7% were low‐risk drinkers; and 18.2% were abstainers. Only 25.5% of people with PPY dependence ever received treatment. Being married was associated positively with the odds of both AR and NR, and ethanol intake was negatively associated with both. Severity of dependence increased the odds of AR but decreased the odds of NR. The odds of AR (but not NR) increased with age and female gender but were decreased by the presence of a personality disorder. Treatment history modified the effects of college attendance/graduation, age at onset and interval since onset on the odds of recovery.Conclusions  There is a substantial level of recovery from alcohol dependence. Information on factors associated with recovery may be useful in targeting appropriate treatment modalities.
Outcome criteria in smoking cessation trials: proposal for a common standard
Authors: West Robert , Hajek Peter , Stead Lindsay , Stapleton John 
Published: February 2005

ABSTRACTSmoking cessation treatment is now integrated into many health‐care systems and a major research effort is under way to improve current success rates. Until now results from randomized clinical trials have been reported in many different ways, leading to problems of interpretation. We propose six standard criteria comprising the ‘Russell Standard’ (RS). These criteria are applicable to trials of cessation aids where participants have a defined target quit date and there is face‐to‐face contact with researchers or clinic staff, as follows. (1) Follow‐up for 6 months (RS6) or 12 months (RS12) from the target quit date or the end of a predefined ‘grace period’; (2) self‐report of smoking abstinence over the whole follow‐up period allowing up to five cigarettes in total; (3) biochemical verification of abstinence at least at the 6‐month or 12‐month follow‐up point; (4) use of an ‘intention‐to‐treat’ approach in which data from all randomized smokers are included in the analysis unless they have died or moved to an untraceable address (participants who are included in the analysis are counted as smokers if their smoking status at the final follow‐up cannot be determined); (5) following‐up ‘protocol violators’ and using their true smoking status in the analysis; and (6) collecting follow‐up data blind to smokers’ allocation to trial group. We believe that these criteria provide the best compromise between practicability and surrogacy for long‐term cessation and will enable meaningful comparison between studies. There may be good reasons why other outcome criteria would also be reported, and studies that involve interventions with special groups or where there is no designated target quit date or face to face contact would need to adapt these criteria accordingly.