Constructive Logics for Program Correctness

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

定価:本体3,500円+税
在庫:お問い合わせください