Computer-aided programming using formally specificed design templates

This paper describes a formal component language, used to support automated component-based program development. The components, referred to as templates, are machine processable, meaning that appropriate tool support, such as retrieval support, can be developed. The templates are highly adaptable, meaning that they can be applied to a wide range of problems. Some of the main features of the language are described, including: higher-order parameters; state variable declarations; specification statements and conditionals; applicability conditions and theories; meta-level place holders; and abstract data structures.

Incremental parsing in language-based editors: user needs and how to meet them

Incremental parsing has long been recognized as a technique of great utility in the construction of language-based editors, and correspondingly, the area currently enjoys a mature theory. Unfortunately, many practical considerations have been largely overlooked in previously published algorithms. Many user requirements for an editing system necessarily impact on the design of its incremental parser, but most approaches focus only on one: response time. This paper details an incremental parser based on LR parsing techniques and designed for use in a modeless syntax recognition editor. The nature of this editor places significant demands on the structure and quality of the document representation it uses, and hence, on the parser. The strategy presented here is novel in that both the parser and the representation it constructs are tolerant of the inevitable and frequent syntax errors that arise during editing. This is achieved by a method that differs from conventional error repair techniques, and that is more appropriate for use in an interactive context. Furthermore, the parser aims to minimize disturbance to this representation, not only to ensure other system components can operate incrementally, but also to avoid unfortunate consequences for certain user-oriented services. The algorithm is augmented with a limited form of predictive tree-building, and a technique is presented for the determination of valid symbols for menu-based insertion. Copyright (C) 2001 John Wiley & Sons, Ltd.

A total electron content space weather study of the Nighttime Weddell Sea Anomaly of 1996/97 southern summer with TOPEX/Poseidon radar altimetry

This paper reports on a total electron content space weather study of the nighttime Weddell Sea Anomaly, overlooked by previously published TOPEX/Poseidon climate studies, and of the nighttime ionosphere during the 1996/1997 southern summer. To ascertain the morphology of spatial TEC distribution over the oceans in terms of hourly, geomagnetic, longitudinal and summer-winter variations, the TOPEX TEC, magnetic, and published neutral wind velocity data are utilized. To understand the underlying physical processes, the TEC results are combined with inclination and declination data plus global magnetic field-line maps. To investigate spatial and temporal TEC variations, geographic/magnetic latitudes and local times are computed. As results show, the nighttime Weddell Sea Anomaly is a large (∼1,600(°)2; ∼22 million km2 estimated for a steady ionosphere) space weather feature. Extending between 200°E and 300°E (geographic), it is an ionization enhancement peaking at 50°S–60°S/250°E–270°E and continuing beyond 66°S. It develops where the spacing between the magnetic field lines is wide/medium, easterly declination is large-medium (20°–50°), and inclination is optimum (∼55°S). Its development and hourly variations are closely correlated with wind speed variations. There is a noticeable (∼43%) reduction in its average area during the high magnetic activity period investigated. Southern summer nighttime TECs follow closely the variations of declination and field-line configuration and therefore introduce a longitudinal division of four (Indian, western/eastern Pacific, Atlantic). Northern winter nighttime TECs measured over a limited area are rather uniform longitudinally because of the small declination variation. TOPEX maps depict the expected strong asymmetry in TEC distribution about the magnetic dip equator.

Multi-threaded Communicating Agents in Qu-Prolog

In this tutorial paper we summarise the key features of the multi-threaded Qu-Prolog language for implementing multi-threaded communicating agent applications. Internal threads of an agent communicate using the shared dynamic database used as a generalisation of Linda tuple store. Threads in different agents, perhaps on different hosts, communicate using either a thread-to-thread store and forward communication system, or by a publish and subscribe mechanism in which messages are routed to their destinations based on content test subscriptions. We illustrate the features using an auction house application. This is fully distributed with multiple auctioneers and bidders which participate in simultaneous auctions. The application makes essential use of the three forms of inter-thread communication of Qu-Prolog. The agent bidding behaviour is specified graphically as a finite state automaton and its implementation is essentially the execution of its state transition function. The paper assumes familiarity with Prolog and the basic concepts of multi-agent systems.

Formalising progress properties of non-blocking programs

A non-blocking program is one that uses non-blocking primitives, such as load-linked/store-conditional and compare-and-swap, for synchronisation instead of locks so that no process is ever blocked. According to their progress properties, non-blocking programs may be classified as wait-free, lock-free or obstruction-free. However, a precise description of these properties does not exist and it is not unusual to find a definition that is ambiguous or even incorrect. We present a formal definition of the progress properties so that any confusion is removed. The formalisation also allows one to prove the widely believed presumption that wait-freedom is a special case of lock-freedom, which in turn is a special case of obstruction-freedom.