Program correctness over abstract data types, with error-state semantics

著者

• Tucker, J. V. (John V.)
• Zucker, J. I.

書誌事項

Program correctness over abstract data types, with error-state semantics

J.V. Tucker, J.I. Zucker

（CWI monograph, 6）

North-Holland , Sole distributors for the U.S.A and Canada, Elsevier Science Pub. Co., 1988

内容説明・目次

内容説明

This research monograph is concerned with the theory of program specification and verification. More specifically, it is about proof systems, in the style of Floyd and Hoare, for proving the correctness of programs interpreted over abstract data types. In addition, the proof systems are designed to operate on programs with the semantic feature that using an uninitialised variable leads to an error message. Designed for the computer scientist, or mathematician interested in the theory of programming languages, the book discusses established and new tools necessary for proving the soundness and completeness of logics for partial and total correctness in an abstract setting. The new tools include classes of many-sorted structures, weak second order assertion languages, and, in particular, a full generalization of the theory of computable functions from the natural numbers to many-sorted abstract structures. Some new generalizations of the Church-Turing Thesis are discussed in detail.

目次

• Straight-Line Programs. Preliminaries: Signatures and Structures. The Programming Language. Assertions. Correctness Formulae. A Proof System
• Soundness. Predicates
• State Transformers
• The Weakest Precondition and Strongest Postcondition. Completeness of the Proof System. `While' Programs. Notation for Partial Functions. The Programming Language. Assertions. Correctness Formulae. A Proof System
• Soundness. Partial State Transformers
• The Weakest Precondition and Strongest Postcondition. Completeness of the Proof System. Appendix: Total Correctness for `While' Programs. Recursive Programs. The Programming Language. Assertions. Correctness Formulae. A Proof System
• Soundness. A Look Ahead. Inductive Computability of the Input-Output Relation. Completeness of the Proof System. Appendix: Total Correctness for Recursive Programs. Computability in an Abstract Setting. Induction Schemes. Some Important Properties. From Induction Schemes to `While' Programs. From `While' Programs to Induction Schemes. Course-of-Values Induction. From COV Induction Schemes to `While'-Array Programs. From `While'-Array Programs to COV Induction Schemes. More on Induction. The COV Inductively Definable Functions. A Survey of Computability in an Abstract Setting. A Generalized Church-Turing Thesis. Bibliography.

「Nielsen BookData」 より

詳細情報

• NII書誌ID(NCID): BA03706836
• ISBN:
  • 0444703403
• LCCN: 87030764
• 出版国コード: ne
• タイトル言語コード: eng
• 本文言語コード: eng
• 出版地: Amsterdam ; Tokyo,New York
• ページ数/冊数: viii, 212 p.
• 大きさ: 25 cm
• 分類:
  • LCC : QA76.6
  • DC19 : 005
• 件名:
  • LCSH : Electronic digital computers -- Programming
  • LCSH : Abstract data types (Computer science)
• 親書誌ID:
  • BA00265574