The formal specification of abstract data types and their implementation in Fortran 90: Implementation issues concerning the use of pointers

In this paper we continue our investigation into the development of computational-science software based on the identification and formal specification of Abstract Data Types (ADTs) and their implementation in Fortran 90. In particular, we consider the consequences of using pointers when implementing a formally specified ADT in Fortran 90. Our aim is to highlight the resulting conflict between the goal of information hiding, which is central to the ADT methodology, and the space efficiency of the implementation. We show that the issue of storage recovery cannot be avoided by the ADT user, and present a range of implementations of a simple ADT to illustrate various approaches towards satisfactory storage management. Finally, we propose a set of guidelines for implementing ADTs using pointers in Fortran 90. These guidelines offer a way gracefully to provide disposal operations in Fortran 90. Such an approach is desirable since Fortran 90 does not provide automatic garbage collection which is offered by many object-oriented languages including Eiffel, Java, Smalltalk, and Simula.

A SPECIFICATION OF A COMPLEX PROGRAMMING LANGUAGE STATEMENT

A formal specification of a complex programming language statement is presented. The subject matter was selected as being typical of the kind confronting a small software house. It is shown that formal specification notations may be applied, with benefit, to 'messy' problems. Emphasis is placed upon producing a specification which is readable by, and useful to a reader not familiar with formal notations.

Derivation of scientific software from mathematical specifications

Often the modification and enhancement of large scientific software systems are severely hampered because many components of the system are written in an implementation dependent fashion, they are inadequately documented, and their functionalities are not precisely known. In this paper we consider how mathematics may be employed to alleviate some of these problems. In particular, we illustrate how the formal specification notation VDM-SL is being used to specify precisely abstract data types for use in the development of scientific software.

Management in distributed systems: A semi-formal approach

The reverse engineering of a skeleton based programming environment and redesign to distribute management activities of the system and thereby remove a potential single point of failure is considered. The Ore notation is used to facilitate abstraction of the design and analysis of its properties. It is argued that Ore is particularly suited to this role as this type of management is essentially an orchestration activity. The Ore specification of the original version of the system is modified via a series of semi-formally justified derivation steps to obtain a specification of the decentralized management version which is then used as a basis for its implementation. Analysis of the two specifications allows qualitative prediction of the expected performance of the derived version with respect to the original, and this prediction is borne out in practice.

Global and local contributions to the optical specification of time to contact: Observer sensitivity to composite tau

First-order time remaining until a moving observer will pass an environmental element is optically specified in two different ways. The specification provided by global tau (based on the pattern of change of angular bearing) requires that the element is stationary and that the direction of motion is accurately detected, whereas the specification provided by composite tau (based on the patterns of change of optical size and optical distance) does not require either of these. We obtained converging evidence,for our hypothesis. that observers are sensitive to composite tau in four experiments involving, relative judgments of, time to, passage with forced-choice methodology. Discrimination performance was enhanced in the presence of a local expansion component, while being unaffected when the detection of the direction of heading was impaired. Observers relied on the information carried in composite tau rather than on the information carried in its constituent components. Finally, performance was similar under conditions of observer motion and conditions of object motion. Because composite tau specifies first-order time remaining for a large number of situations, the different ways in which it may be detected are discussed.

A concise and convergent (formal) total synthesis of huperzine A

The first convergent synthesis of the tricyclic skeleton of huperzine A is described and includes, as the key step, an efficient regioselective intramolecular Heck reaction of 2-(tert-butyldimethylsillyoxymethyl)-6-(2-methoxy-5-bromopyridin-6-yl)methylcyclohex-2-enol.