Abstract

Abstract
The emergence of lightweight formal methods tools such as Alloy improves the software design process, by encouraging developers to model and verify their systems before engaging in hideous implementation details. However, an abstract Alloy specification is far from an actual implementation, and manually refining the former into the latter is unfortunately a non-trivial task. This paper identifies a subset of the Alloy language that is equivalent to a relational database schema with the most conventional integrity constraints, namely functional and inclusion dependencies. This semantic correspondence enables both the automatic translation of Alloy specifications into relational database schemas and the reengineering of legacy databases into Alloy. The paper also discusses how to derive an object-oriented application layer to serve as interface to the underlying database.

Abstract

Abstract
Coordination in R eo emerges from the composition of the behavioural constraints of the primitives, such as channels, in a component connector. Understanding and implementing R eo, however, has been challenging due to interaction of the channel metaphor, which is an inherently local notion, and the non-local nature of constraint propagation imposed by composition. In this paper, the channel metaphor takes a back seat, and we focus on the behavioural constraints imposed by the composition of primitives, and phrase the semantics of R eo as a constraint satisfaction problem. Not only does this provide a clear intensional description of the behaviour of R eo connectors in terms of synchronisation and data flow constraints, it also paves the way for new implementation techniques based on constraint propagation and satisfaction. In fact, decomposing R eo into constraints provides a new computational model for connectors, which we extend to model interaction with an unknown external world beyond what is currently possible in R eo.

Abstract
The ability to interactively render dynamic scenes with global illumination is one of the main challenges in computer graphics. The improvement in performance of interactive ray tracing brought about by significant advances in hardware and careful exploitation of coherence has rendered the potential of interactive global illumination a reality. However, the simulation of complex light transport phenomena, such as diffuse interreflections, is still quite costly to compute in real time. In this paper we present a caching scheme, termed Instant Caching, based on a combination of irradiance caching and instant radiosity. By reutilising calculations from neighbouring computations this results in a speedup over previous instant radiosity-based approaches. Additionally, temporal coherence is exploited by identifying which computations have been invalidated due to geometric transformations and updating only those paths. The exploitation of spatial and temporal coherence allows us to achieve superior frame rates for interactive global illumination within dynamic scenes, without any precomputation or quality loss when compared to previous methods; handling of lighting and material changes are also demonstrated.

Abstract
This paper describes a study conducted at the University of Nottingham, whose goal was to assess whether the students registered on the first-year module "Mathematics for Computer Scientists" appreciate the calculational method. The study consisted of two parts: "Proof Reading" and "Problem Solving". The goal of "Proof Reading" was to determine what the students think of calculational proofs, compared with more conventional ones, and which are easier to verify; we also assessed how their opinions changed during the term. The purpose of "Problem Solving" was to determine if the methods taught have influenced the students' problem-solving skills. Frequent criticisms of our approach are that we are too formal and that the emphasis on syntactic manipulation hinders students' understanding. Nevertheless, the results show that most students prefer or understand better the calculational proofs. On the other hand, regarding the problem-solving questions, we observed that, in general, the students maintained their original solutions. © 2009 Crown.