April 1977 - Vol. 20 No. 4
Features
A proof method, subgoal induction, is presented as an alternative or supplement to the commonly used inductive assertion method. Its major virtue is that it can often be used to prove a loop's correctness directly from its input-output specification without the use of an invariant. The relation between subgoal induction and other commonly used induction rules is explored and, in particular, it is shown that subgoal induction can be viewed as a specialized form of computation induction. A set of sufficient conditions are presented which guarantee that an input-output specification is strong enough for the induction step of a proof by subgoal induction to be valid.
The editing of picture segmentations using local analysis of graphs
A major problem in picture processing is the elimination of the large number of spurious regions that result from an initial segmentation by region growing techniques. Such regions have been eliminated either on the basis of semantic information or on the basis of size and contrast. A scheme is presented which performs eliminations on the basis of local properties of the region adjacency graph. The scheme is based on definitions of graph properties which are satisfied when a spurious region is present; then editing is equivalent to fast graph operations. A number of examples are shown.
Studies in machine cognition using the game of poker
A progress report is presented of on-going research efforts concerning human decision making under uncertainty and risk and human problem solving and learning processes on the one hand, and machine learning, large scale programming systems, and novel programming techniques on the other. There has also been interest in how humans make deductive and inductive inferences and form and optimize heuristic rules, and how machines can reach similar results. Although the vehicle of these investigations has been the game of poker, a conceptual framework has been provided that should have a fairly wide range of applicability. The models of human judgement, choice, and decision making are incorporated in a large scale complex program. They represent both descriptive and normative theories of behavior. An interactive game environment has been recently established which, besides its usefulness for experiments in game playing, enables humans to construct machine strategies “on-line” in a question answering, advice taking mode.
Analysis of design alternatives for virtual memory indexes
A class of index structures for use in a virtual memory environment is described. Design alternatives within this class of index structures are analyzed. These alternatives include a choice of search strategy, whether or not pages in the index are stuctured, and whether or not keys are compressed. The average cost of retrieving entries from these indexes is expressed as a weighted sum of the cost of a basis key comparison and the cost of crossing a page boundary in the index structure. Formulas for the retrieval costs possible combinations of design alternatives are given. These are used in numerical case studies which compare the retrieval costs of the alternatives. Qualitative comparisons of the maintenance costs (insertion, deletion, reorganization) of the design alternatives are also included.
The stage hypothesis and the s-curve: some contradictory evidence
This paper presents the results of a study testing the s-shaped budget curve of Nolan's stage model of computer development in an organization. Research on the data processing budgets of California counties fails to support the s-shaped curve or the use of budgets as a basis for a stage model. However, the results do not invalidate the concept of a stage model. The analysis suggest an alternative model of budget growth and a separation between models of budgeting growth and growth stages in the development of the computer resource.
Approximating block accesses in database organizations
When data records are grouped into blocks in secondary storage, it is frequently necessary to estimate the number of blocks XD accessed for a given query. In a recent paper [1], Cardenas gave the expression XD = m(1 - (1 - 1/m)k), (1) assuming that there are n records divided into m blocks and that the k records satisfying the query are distributed uniformly among the m blocks. The derivation of the expression was left to the reader as an exercise.
Remark on uniform insertion in structured data structures
In a recent paper, Shneiderman and Scheuermann [1] have defined an interesting operation, called uniform insertion, whereby a (linked) data structure G2 can be embedded within another structure G1 in such a way that each data node of G1 serves as an entry node for G2. This communication points out and corrects an error in their definition, while preserving the spirit of that operation.
Comment on weighted increment linear search for scatter tables
I would like to comment on an article by Fabrizio Luccio [1] which discusses weighted increment linear search for scatter tables.
Sorting on a mesh-connected parallel computer
Two algorithms are presented for sorting n2 elements on an n × n mesh-connected processor array that require O (n) routing and comparison steps. The best previous algoritmhm takes time O(n log n). The algorithms of this paper are shown to be optimal in time within small constant factors. Extensions to higher-dimensional arrays are also given.
Proof techniques for hierarchically structured programs
A method for describing and structuring programs that simplifies proofs of their correctness is presented. The method formally represents a program in terms of levels of abstraction, each level of which can be described by a self-contained nonprocedural specification. The proofs, like the programs, are structured by levels. Although only manual proofs are described in the paper, the method is also applicable to semi-automatic and automatic proofs. Preliminary results are encouraging, indicating that the method can be applied to large programs, such as operating systems.
