Search

SELECT is an experimental system for assisting in the formal systematic debugging of programs. It is intended to be a compromise between an automated program proving system and the current ad hoc debugging practice, and is similar to a system being developed by King et al. of IBM. SELECT systematically handles the paths of programs written in a LISP subset that includes arrays. For each execution path SELECT returns simplified conditions on input variables that cause the path to be executed, and simplified symbolic values for program variables at the path output. For conditions which form a system of linear equalities and inequalities SELECT will return input variable values that can serve as sample test data. The user can insert constraint conditions, at any point in the program including the output, in the form of symbolically executable assertions. These conditions can induce the system to select test data in user-specified regions. SELECT can also determine if the path is correct with respect to an output assertion. We present four examples demonstrating the various modes of system operation and their effectiveness in finding bugs. In some examples, SELECT was successful in automatically finding useful test data. In others, user interaction was required in the form of output assertions. SELECT appears to be a useful tool for rapidly revealing program errors, but for the future there is a need to expand its expressive and deductive power.

Properties of a graph (directed or undirected) whose adjacency matrix is a circulant are studied. Examples are given showing that the connection set determined by the first row of such a matrix need not be multiplicatively related to the connection set of an isomorphic graph. Two different criteria are given under which two graphs with circulant adjacency matrices are isomorphic if and only if their connection sets are multiplicatively related. The first criterion is that the graphs have a prime number of vertices. The second criterion is that the adjacency matrices have non-repeated eigenvalues. The final section gives a partial characterization of graphs with n vertices whose automorphism group is the cyclic group Cn.

SELECT is an experimental system for assisting in the formal systematic debugging of programs. It is intended to be a compromise between an automated program proving system and the current ad hoc debugging practice, and is similar to a system being developed by King et al. of IBM. SELECT systematically handles the paths of programs written in a LISP subset that includes arrays. For each execution path SELECT returns simplified conditions on input variables that cause the path to be executed, and simplified symbolic values for program variables at the path output. For conditions which form a system of linear equalities and inequalities SELECT will return input variable values that can serve as sample test data. The user can insert constraint conditions, at any point in the program including the output, in the form of symbolically executable assertions. These conditions can induce the system to select test data in user-specified regions. SELECT can also determine if the path is correct with respect to an output assertion. We present four examples demonstrating the various modes of system operation and their effectiveness in finding bugs. In some examples, SELECT was successful in automatically finding useful test data. In others, user interaction was required in the form of output assertions. SELECT appears to be a useful tool for rapidly revealing program errors, but for the future there is a need to expand its expressive and deductive power.

This report summarizes project work carried out at the Computer Science Laboratory of SRI International under Contract F30602-78-C-0031 with Rome Air Development Center during the period November 1977 - November 1981. The project has been concerned with the development of a programming environment (Rugged Jovial Environment)--with verification tools as a principal component--for the specification, development, and formal verification of programs in JOVIAL-J73. The term verification here refers to proof of correctness with respect to formal specification by the method of Floyd assertions. The effort on this project has ranged from fairly abstract work on formal models of computation (in particular, regarding the semantics of JOVIAL constructs) to practical techniques for implementing these models. This has resulted in the development of a user-friendly system, written in INTERLISP, with the aid of which it is possible to verify JOVIAL software of significant complexity. In addition to our primary project work, we developed several very usefull software tools of more general applicability. These tools are also described in the report.

This chapter is concerned with systematic techniques for the realization of multioutput combinational logic functions by means of a regular interconnection geometry, that of multirail cellular cascades. As with single-rail (Maitra) cascades, of which multirail cascades are a generalization, interconnections are allowed only between adjacent cells. A mathematical theory, the decomposition theory of group functions, is developed which permits systematic techniques of great generality to be applied to this logic synthesis problem. The synthesis techniques described here permit the exercise of considerable control over the number and internal structure of the individual cells required for arbitrary multioutput function synthesis. Comparisons are made with alternative techniques for the synthesis of multirail cascades.