A correctness proof of an indenting program

The correctness of an indenting program for Pascal is proved at an intermediate level of rigour. The specifications of the program are given in the companion paper.¹ The program is approximately 330 lines long and consists of four modules: io, lex, stack and indent. We prove first that the individual procedures contained in these modules meet their specifications as given by the entry and exit assertions. A global proof of the main routine then establishes that the interaction between modules is such that the main routine meets the specification of the entire program. We argue that correctness proofs at the level of rigour used here serve very well to transfer one's understanding of a program to others. We believe proofs at this level should become commonplace before more formal proofs can take over to reduce traditional testing to an inconsequential place.     

Relative specification and transformational re-use of functional programs

Arelative specification is a collection of laws relating the behaviour of a required new program to that of one or more existing programs. A two stage method for transforming such relative specifications into effective functional programs is described and illustrated. Theinversion stage re-arranges the specifying laws to obtain a collection ofpartial definitions for each unknown function, typically involving non-deterministic operators. The subsequentfusion stage combines each set of partial definitions into a single complete definition, thereby eliminating non-deterministic operators.Supported by Science and Engineering Research Council, Grant GR/E16571     

A contextual analysis of Pascal programs

More than 120,000 lines of Pascal programs, written by graduate students and faculty members, have been statically analysed to provide a better understanding of how the language is ‘really’ used. The analysis was done within twelve distinct contexts to discover differences in usage patterns among the various contexts. For example, it was found that 47 per cent of the operands in arguments lists were constants. The results are displayed as tables of frequency counts which show how often each construct is used within a context. Also, we have compared our findings to the results from studies of other languages, such as FORTRAN, SAL and XPL.     

A functional presentation of Fourier series convergence

Understanding lengthy mathematical proofs requires strong concentration. Authors must efficiently map whole logical structures into sequential texts. One way to ease such tasks is presenting the logical structure in a functional programming style. In our method, functional proofs are implemented by a real programming language. The behavior of each function appears in the proofs as a building block ready to be visualized with concrete data. This paper contains a case study of the well-known Dirichlet's theorem on the convergence of Fourier series. It shows the relevance of our method in rigorous mathematical presentations that involve - arguments intensively.     

An incremental garbage collection algorithm for multi-mutator systems

An elementary correctness proof for Ben-Ari's algorithm (1984) for incremental garbage collection is given. We give a new algorithm for systems in which there are multiple mutators and a proof of its correctness, which is a minor modification of the previous proof. Finally, we remark upon a way to implement these algorithms that may increase their performance on certain architectures. Carl Pixley holds B.S., M.S. and Ph.D. degrees in mathematics from the University of Omaha, Rutgers-The State University, and the State University of New York at Binghamton, respectively. His principal contributions are the Pixley-Roy construction of set-theoretic topology, a example in the selection theory of infinite-dimensional spaces, a decomposition theorem (with W. Eaton) in geometric topology, and the design and implementation of demanddriven arithmetic in a functional programming language. He is now a member of the technical staff of the VLSI Computer Aided Design Program of Microelectronics and Computer Technology Corporation (MCC) in Austin Texas, where he is investigating mathematical methods in the verification of hardware.     

A modal specification theory for components with data

Modal specification is a well-known formalism used as an abstraction theory for transition systems. Modal specifications are transition systems equipped with two types of transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows for developing a unique approach for both logical and structural compositions, and eases the step-wise refinement process for building implementations. We propose Modal Specifications with Data (MSDs), the first modal specification theory with explicit representation of data. Our new theory includes the most commonly seen ingredients of a specification theory; that is parallel composition, conjunction and quotient. As MSDs are by nature potentially infinite-state systems, we propose symbolic representations based on effective predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.     

抽象数据类型条件方程的求取

抽象数据类型的代数规格说明关键在于条件方程的求取。如果能获得简明的条件描述，那么就容易写出条件方程。本文讨论了抽象数据类型的规格说明问题，并提出了基于串和数组求取条件方程的方法，同时给出了若干典型实例，并对求取条件方程方法的正确性作了讨论。     

A case study of run-time errors in Pascal programs

The results of a case study in which over 100,000 Pascal program executions were monitored for run-time errors are reported. A large number of run-time errors in a wide variety of categories were observed. The data reported provided insight into the use and misuse of the features of Pascal by a large population of programmers. Some implications of these statistics on compiler implementation and programming language design are discussed. The number and variety of errors detected suggests that run-time checking mechanisms are more important and useful than is generally recognized, judging by the incompleteness of such mechanisms in many compilers.     

Response to “the formal specification of safety requirements for storing explosives”

This short communication is a response to [MuS93] investigating their ACS system specification. The main point in this paper is that executing specifications can be used as a feasible way of validating them. It is essential to have tool support which enables one to write a generally not executable specification, and then prototype (parts of) it directly in the specification language, without translating it into some other prototyping language.     

Generating reversible programs

This paper describes the production of a system to control an electronic cricket scoreboard. The main feature of the system is the ability of the operator to ‘undo’ operations that he has performed, in order to correct errors that has has made. Undo is implemented by reversing the execution of the program. The code to perform the reversal is generated automatically and results in a minimal amount of state information being recorderded.     

A case for acquiring Pascal

This paper is a copy of the case made by the author to his County Council for acquisition of a Pascal compiler for their computer. Its message is essentially that Pascal is the best thing since sliced bread.     

GSL: a requirements specification language for end-user intelligibility

Software Requirements Specifications (SRS) have been used to fill the communication gap between systems analysts and the end-users. SRSs should satisfy the needs of both systems analysts and end-users. Non-technical end-users require intelligible SRSs while systems analysts need more precise, clear and concise SRSs. Object-oriented methods cannot represent temporal relations between events precisely. However, object-oriented principles are widely used in systems analysis and designing. Hence, there is a need for a software requirements specification language which supports object-oriented analysis methods, represents temporal knowledge precisely and whose representation scheme resembles natural languages. The specification language presented in this paper, GSL, is designed to meet the above requirements. The language is based on First-order Temporal Logic (FTL), which has temporal operators in addition to classical logical connectives and quantifiers. Since FTL cannot represent relative temporal knowledge and it inherits problems with point-based time models, a new logical connective TAND and redefined AND connective are used to represent relative temporal knowledge and to solve the problems with FTL. The language employs object-oriented principles: events, conditions, rules and activities can be represented as objects as well as attributes of an object. However, systems analysts can decide whether to use object-oriented conceptual modeling or not. © 1998 John Wiley & Sons, Ltd.     

The applicability of program schema results to programs

Several classes of programs, which are the analogues of previously investigated classes of program schemas, are defined. Decidability and translatability questions are considered for these classes of programs, as well as the applicability of these results to the theories of optimization and program testing. The usefulness of the schema model is studied by considering the inheritability of schema properties by programs, and conversely, the inheritability of program properties by schemas.     

The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML

We describe the basic structure of an environment for proving programs annotated with JML specifications. Our method is generic with respect to the API, and thus well suited for applets certification. It involves three distinct components: the tool, which computes proof obligations for a core imperative language annotated with pre- and post-conditions, the proof assistant for modeling the program semantics and conducting the development of proofs, and finally the tool, a translator of our own, which reads the files and produces specifications for and a representation of the semantics of the program into ’s input language.     

Improving the structure of large Pascal programs

This paper describes an extension to Pascal in the form of an encapsulation mechanism aimed at improving the structure of large Pascal programs. It is based upon the module structure of Modula but extended to include a more detailed specification of module interfaces and to allow the definition of a module body to be deferred. Called Pascal/M, the extended language is implemented via a preprocessor. It has been successfully used in large programming projects and been found to both aid in the application of top-down design methods and to greatly improve the documentation of the final product by breaking up the program text into a hierarchy of short readable modules. The use of Pascal/M is illustrated by a program example and aspects of its design and implementation are discussed.     

An analysis of Pascal programs in compiler writing

A method and results of static and dynamic analysis of Pascal programs are described. In order to investigate characteristics of large systems programs developed by the stepwise refinement programming approach and written in Pascal, several Pascal compilers written in Pascal were analysed from both static and dynamic points of view. As a main conclusion, procedures play an important role in the stepwise refinement approach and implementors of a compiler and designers of high level language machines for Pascal-like languages should pay careful attention to this point. The set data structure is one of the characteristics of the Pascal language and statistics of set operations are also described.