The problem of naming and locating objects in a distributed environment is considered, and the clearinghouse, a decentralized agent for supporting the naming of these "network-visible" objects, is described.The objects "known" to the clearinghouse are of many types and include workstations, file servers, print servers, mail servers, clearinghouse servers, and human user.All objects known to the clearinghouse are named using the same convention, and the clearinghouse provides information about objects in a uniform fashion, regardless of their type.The clearinghouse also supports aliases.The clearinghouse binds a name to a set of properties of various types.For instance, the name of a user may be associated with the location of his local workstation, mailbox, and nonlocation information such as password and comments.The clearinghouse is decentralized and replicated.That is, instead of one global clearinghouse server, there are many local clearinghouse servers, each storing a copy of a portion of the global database.The totality of services supplied by these clearinghouse servers is called "the clearinghouse."Decentralization and replication increase efficiency, security, and reliability.A request to the clearinghouse to bind a name to its set of properties may originate anywhere in the system and be directed to any clearinghouse server.A clearinghouse client need not be concerned with the question of which clearinghouse server actually contains the binding--the clearinghouse stub in the client in conjunction with distributed clearinghouse servers automatically fmds the mapping ff it exists.Updates to the various copies of a mapping may occur asynchronously and be interleaved with requests for bindings of names to properties; updates to the various copies are not treated as indivisible transactions.Any resulting inconsistency between the various copies is only transient: the clearinghouse automatically arbitrates between conflicting updates to restore consistency.

The notion of the congruence closure of a relation on a graph is defined and several algorithms for computing it are surveyed. A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality. A decision procedure is then given for the quantifier-free theory of LISP list structure based on the congruence closure algorithm. Both decision procedures determine the satisfiability of a conjunction of literals of length n in average time O ( n log n ) using the fastest known congruence closure algorithm. It is also shown that if the axiomatization of the theory of list structure is changed slightly, the problem of determining the satisfiability of a conjunction of literals becomes NP-complete. The decision procedures have been implemented in the authors' simplifier for the Stanford Pascal Verifier.

A decision procedure is given for the quantifier-free theory of recursively defined data structures which, for a conjunction of length n, decides its satisfiability in time linear in n.The first-order theory of recursively defined data structures, in particular the first-order theory of LISP list structure (the theory of cons, car, and cdr), is shown to be decidable but not elementary recursive.(This answers an open question posed by John McCarthy.)

An algorithm for prettyprinting is given. For an input stream of length n and an output device with linewidth m , the algorithm requires time O ( n ) and space O ( m ). The algorithm is described in terms of two parallel processes: the first scans the input stream to determine the space required to print logical blocks of tokens; the second uses this information to decide where to break lines of text; the two processes communicate by means of a buffer of size O ( m ). The algorithm does not wait for the entire stream to be input, but begins printing as soon as it has received a full line of input. The algorithm is easily implemented.

A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and ≤, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier.

This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.

We describe a simplifier for use in program manipulation and verification. The simplifier finds a normal form for any expression over the language consisting of individual variables, the usual boolean connectives, the conditional function cond (denoting if-then-else), the integers (numerals), the arithmetic functions and predicates +, - and ≤, the LISP constants, functions and predicates nil, car, cdr, cons and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. Individual variables range over the union of the rationals, the set of arrays, the LISP s-expressions and the booleans true and false. The constant, function and predicate symbols take their natural interpretations.The simplifier is complete; that is, it simplifies every valid formula to true. Thus it is also a decision procedure for the quantifier-free theory of rationals, arrays and s-expressions under the above functions and predicates.The organization of the simplifier is based on a method for combining decision algorithms for several theories into a single decision algorithm for a larger theory containing the original theories. More precisely, given a set S of functions and predicates over a fixed domain, a satisfiability program for S is a program which determines the satisfiability of conjunctions of literals (signed atomic formulas) whose predicates and function signs are in S. We give a general procedure for combining satisfiability programs for sets S and T into a single satisfiability program for S ∪ T, given certain conditions on S and T. We show how a satisfiability program for a set S can be used to write a complete simplifier for expressions containing functions and predicates of S as well as uninterpreted function symbols.The simplifier described in this paper is currently used in the Stanford Pascal Verifier.

A decision algorithm is given for the quantifier-free theory of recursively defined data structures which, for a conjunction of length n, decides its satisfiability in time linear in n. The first-order theory of recursively defined data structures, in particular the first-order theory of LISP list structure (the theory of CONS, CAR, CDR), is shown to be decidable but not elementary recursive.

In this paper we wish to consider the problem of proving assertions about programs that construct and alter arbitrarily complex data structures. In recent years several papers have been written on the subject of proving assertions about such programs; however, the class of data structures considered has generally been a proper sub-class of the class of all data structures, such as the classes of linear lists or trees. [Burstall 1972] discusses the problem of what he calls Distinct Non-repeating Lists and Distinct Non-repeating Trees. [Kowaltowski 1973] extends Burstall's approach. His approach is likewise basically tree-oriented but is applicable to more general data structures. [Laventhal 1974] restricts his attention to 'simple singly-linked lists', noting the problem of providing 'a complete framework for correctness proofs' if one attempts to handle very general data structures. [Morris 1972] discusses the question of designing a programming language for general data structures in order to facilitate verification of programs written in such a language. [Standish 1973] provides a set of axioms for the class of data structures in which, for instance, two data structures are equal iff they are component-wise equal.

In this paper we wish to consider the problem of proving assertions about programs that construct and alter data structures. Our method will be to define a suitable assertion language L for data structures, to define a simple programming language L' for constructing and altering data structures, to give axioms and rules of inference (in the style of [Hoare 1969]) which specify the effect of program segments on data structures (described by formulas in L) and finally to prove that these axioms are correct (relative to a formal definition of the semantics of L') and, in a reasonable sense, complete. Thus our intention is to provide a complete theoretical framework for describing arbitrary data structures and proving assertions about programs that manipulate them.

We consider the first-order theory whose language has as nonlogical symbols the constant symbols 0 and 1, the binary relation symbols = and This theory of integers under addition is commonly called the 'Presburger Arithmetic' and is known to be decidable for truth [Presburger (1929), Hilbert and Bernays (1968)]. We prove here that there exists a decision procedure for this theory, involving quantifier elimination, for which there is a superexponential upper bound on the size of formula produced when all variables have been eliminated.