Now showing items 24-43 of 59

    • Equational Propositional Logic 

      Gries, David; Schneider, Fred B. (Cornell University, 1994-09)
      We formalize equational propositional logic, prove that it is sound and complete, and compare the equational-proof style with the more traditional Hilbert style.
    • Fault-Tolerant Broadcasts 

      Schneider, Fred B.; Gries, David; Schlichting, Richard D. (Cornell University, 1983-09)
      A distributed program is presented that ensures delivery of a message to the functioning processors in a computer network, despite the fact that processors may fail at any time. All processor failures are assumedd to be ...
    • Finding Repeated Elements 

      Misra, Jayadev; Gries, David (Cornell University, 1982-07)
      Two algorithms are presented for finding the values that occur more than $n \div k$ times in array b[O:n-1]. The second algorithm requires time $O(n \log(k))$ and extra space $O(k)$. We prove that $O(n \log(k))$ is a ...
    • Formal Justification of Underspecification for S5 

      Aaron, Eric; Gries, David (Cornell University, 1997-02)
      We formalize the notion of underspecification as a means of avoiding problems with partial functions in modal logic S5 and some semantically related logics. For these logics, underspecification respects validity, so ...
    • Formal versus semiformal proof in teaching predicate logic 

      Gries, David (Cornell University, 1996-08)
      This space is left deliberately non-blank
    • Formalizations Of Substitution Of Equals For Equals 

      Gries, David; Schneider, Fred B. (Cornell University, 1998-05)
      Inference rule "substitution of equals for equals" has been formalized in terms of simple substitution (which performs a replacement even though a free occurrence of a variable is captured), contextual substitution (which ...
    • General Correctness: A Unification of Partial and Total Correctness 

      Jacobs, Dean; Gries, David (Cornell University, 1984-10)
      General correctness, which subsumes partial and total correctness, is defined for both weakest preconditions and strongest postconditions. Healthiness properties for general-correctness predicate transformers are more ...
    • Generating a Random Cyclic Permutation 

      Gries, David; Xue, Jinyun (Cornell University, 1986-09)
    • The Hopcroft-Tarjan Planarity Algorithm, Presentation and Improvements 

      Gries, David; Xue, Jinyun (Cornell University, 1988-04)
      We give a rigorous, yet, we hope, readable, presentation of the Hopcroft-Tarjan linear algorithm for testing the planarity of a graph, using more modern principles and techniques for developing and presenting algorithms ...
    • In-situ Inversion of a Cyclic Permutation 

      Feijen, W. H. J.; Van Gasteren, A. J. M.; Gries, David (Cornell University, 1985-09)
      An algorithm is developed for the in-situ 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, 1987-11)
    • An Introduction to Proofs of Program Correctness for Teachers of College-Level Introductory Programming Courses 

      Gries, David; Wadkins, Jeff (Cornell University, 1990-03)
      No abstract is available.
    • Is Sometimes Ever Better Than Always? 

      Gries, David (Cornell University, 1978-06)
      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, 1977-06)
    • McLaren's Masterpiece 

      Gries, David; Prins, Jan F. (Cornell University, 1986-01)
      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, 1985-06)
      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, 1984-11)
      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, 1994-02)
      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 Iteration 

      Gries, David (Cornell University, 1977-09)
    • A Note on Program Development 

      Gries, David (Cornell University, 1974-03)