LCS Technical Memos (1974 - 2003): Recent submissions

Now showing items 400-402 of 486

    • Nondeterminism in Logics of Programs 

      Harel, David; Pratt, Vaughan R. (1978-02)
      We investigate the principles underlying reasoning about nondeterministic programs, and present a logic to support this kind of reasoning. Our logic, an extension of dynamic logic ([22] and [12]), subsumes most existing ...

    • Computability and Completeness in Logics of Programs 

      Harel, David; Meyer, Albert R.; Pratt, Vaughan R. (1978-02)
      Dynamic logic is a generalization of first order logic in which quantifiers of the form "for all X…" are replaced by phrases of the form "after executing program α…". This logic subsumes most existing first-order logic of ...

    • A Complete Axiomatic System for Proving Deductions About Recursive Programs 

      Harel, David; Pnueli, Amir; Stavi, Jonathan (1978-02)
      Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of a H u {^,v,∃,∀} uH^-1, including the rules of H, four special purpose rules ...