JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Author "Gries, David"
Now showing items 3251 of 59

The HopcroftTarjan Planarity Algorithm, Presentation and Improvements
Gries, David; Xue, Jinyun (Cornell University, 198804)We give a rigorous, yet, we hope, readable, presentation of the HopcroftTarjan linear algorithm for testing the planarity of a graph, using more modern principles and techniques for developing and presenting algorithms ... 
Insitu Inversion of a Cyclic Permutation
Feijen, W. H. J.; Van Gasteren, A. J. M.; Gries, David (Cornell University, 198509)An algorithm is developed for the insitu inversion of a cyclic permutation represented in an array. The emphasis is on the quo modo rather than the quod; we are interested in finding concepts and notations for dealing ... 
Inorder Traversal of a Binary Tree and its Inversion
Gries, David; Van de Snepscheut, Jan L.A. (Cornell University, 198711)ABSTRACT NOT AVAILABLE 
An Introduction to Proofs of Program Correctness for Teachers of CollegeLevel Introductory Programming Courses
Gries, David; Wadkins, Jeff (Cornell University, 199003)No abstract is available. 
Is Sometimes Ever Better Than Always?
Gries, David (Cornell University, 197806)The "intermittent assertion" method for proving programs correct is explained and compared to the conventional axiomatic method. Simple axiomatic proofs of iterative algorithms that compute recursively defined functions, ... 
A Linear Sieve Algorithm for Finding Prime Numbers
Gries, David; Misra, Jayadev (Cornell University, 197706)NO ABSTRACT SUPPLIED 
McLaren's Masterpiece
Gries, David; Prins, Jan F. (Cornell University, 198601)Abstract not available 
A Model and Temporal proof system for Networks of Processes
Nguyen, Van Long; Demers, Alan J.; Gries, David; Owicki, Susan S. (Cornell University, 198506)An approach is presented for modeling networks of processes that communicate exclusively through message passing. A process (or a network) is defined by its set of possible behaviors, where each behavior is an abstraction ... 
A Model and Temporal Proof System for Networks of Processes
Nguyen, Van Long; Gries, David; Owicki, Susan S. (Cornell University, 198411)A model and a sound and complete proof system for networks of processes in which component processes communicate exclusively through messages is given. The model, an extension of the trace model, can desribe both synchronous ... 
A New Approach to Teaching Mathematics
Gries, David; Schneider, Fred B. (Cornell University, 199402)We propose a new approach to teaching discrete math: First, teach logic as a powerful and versatile tool for discovering and communicating truths; then use this tool in all other topics of the course. We spend 6 weeks ... 


A Note on the Standard Strategy for Developing Loop Invariants and Loops
Gries, David (Cornell University, 198210)The bynowstandard strategy for developing a loop invariant and loop was developed in [1] and explained [2]. Nevertheless, its use still poses problems for some. The purpose of this note is to provide further explanation. ... 
On Presenting Monotonicity and On EA=>AE
Gries, David (Cornell University, 199504)Two independent topics are treated. First, the problem of weakening/strengthening steps in calculational proofs is discussed and a form of substantiating such steps is proposed. Second, a simple proof of (Ex R.x: (Ay ... 
Presenting an Algorithm to Find the Minimum Edit Distance
Gries, David; Burkhardt, Bill (Cornell University, 198803)ABSTRACT UNAVAILABLE 
A Procedure Call Proof Rule (With a Simple Explanation)
Gries, David; Levin, Gary Marc (Cornell University, 197905)NO ABSTRACT SUPPLIED 
Program Schemes with Pushdown Stores
Brown, Steven; Gries, David; Szymanski, Thomas G. (Cornell University, 197204)We attempt to characterize classes of schemes allowing pushdown stores, building on an earlier work by Constable and Gries [1]. We study the effect (on the computational power) of aloowing one, two, or more pushdown stores, ... 
Programming by Induction
Gries, David (Cornell University, 197109)A technique for creating programs, called programming by induction, is described. The term is used because of the similarity between programming by induction and proving a theorem by induction. 
Proving Properties of Parallel Programs: An Axiomatic Approach
Owicki, Susan S.; Gries, David (Cornell University, 197505)This paper presents an axiomatic technique for proving a number of properties of parallel programs. Hoare has given a set of axioms for partial correctness of parallel programs, but they are not strong enough in most ... 