Constructive Logics for Program Correctness
著者名 | Takayasu Ito 著 |
---|---|
発行元 | 丸善プラネット |
発行年月日 | 2012年11月 |
判型 | B5 257×182 |
ページ数 | 318ページ |
ISBN | 978-4-86345-146-9 |
Cコード | 3004 |
ジャンル | 電気・電子・情報工学 > 情報・コンピュータ > 言語・プログラミング |
内容紹介
プログラム正当性はコンピュータソフトウェアに要求される最も基本的な概念である。 本書では,Hoareの検証体系が扱うプログラムの弱正当性の概念が論理的に矛盾した概念である事,および,古典論理や直観主義論理に基くプログラム検証体系の問題点を指摘した後,構成的論理に基くプログラム正当性の新しい検証体系を与えている。また,プログラムの構成的意味論および観測可能な計算可能性という新しい計算概念の提案も行っている。 ソフトウェアの基礎理論およびsafe&trustrubleなソフトウェアの基礎技術に携わる研究者・技術者の必読書。
目次
PART Ⅰ Program Correctness Formulae and Their Basic Properties
Chapter 1.Notions of Program Correctness
Chapter 2.Properties of Correctness Formulae sp(S,Q)and vp(S,Q)
PART Ⅱ Logics for Program Correctness in Classical Logic Framework
Chapter 3.JTsp:Logic for Strong Correctness of Procedural Programs
Chapter 4.JTzp:Logic for Strong Correctness of Functional Programs
Chapter 5.Relative Completeness Problem of Program Verification Systems
PART Ⅲ Fully Constructive Logics for Program Correctness and Problem Specification Logic
Chapter 6.Fully Constructive Logic on sp(S,Q)and PS logic
Chapter 7.Fully Constructive Logic on zp(FD,Q)and PS logic
PART Ⅳ Correctness of Stream Programs and Constructive Semantics
Chapter 8. Correctness of Stream Programs
Chapter 9.Program Correctness and Constructive Identity for Programs
Chapter 10.Constructive Semantics and Constructive Logic of Programs
APPENDIX Gentzen’s Logical Systems:LK,LJ and NJ
A.1.LK:Classical predicate calculus in Sequent Calculus
A.2.LJ:Intutionistic predicate logic in Sequent Calculus
A.3.NJ:Intuitionistic logic based on Natural Deduction