こんにちは！論文製本の三恵社の木全です。
弊社で出版をして頂いた書籍のご紹介です。
【内容紹介】
プログラム理論の提唱者・開拓者の一人である伊藤貴康氏がプログラミング言語の意味論をまとめました
世界に先駆けてプログラム強正当性に関する公理的意味論の体系も紹介しています
■プログラムの正当性とは，安心・安全にコンピュータを利用する基礎です
■プログラム理論とは，プログラムの正当性や意味論のための基礎理論です
■構的操作的意味・表示的意味・公理的意味とそれらに基く証明法を述べています
【書籍紹介】
本のタイトル：プログラム理論
発行日：２０１０年６月１５日
著者名：伊藤貴康著（東北大学名誉教授工学博士）
ＩＳＢＮ：978‐4‐88361‐754‐8 C3041
定価：3350円(税別)
【目次】
●第１章手続き型プログラムの操作的意味論の考え方
簡単な手続き型プログラムを対象として状態遷移によるプログラムの操作的意味論の考え方を説明
それを基に簡単な手続き型言語の意味論、プログラムの同値性と正当性の概念などを説明
●第２章関数型プログラムの操作的意味論
条件式と関数合成を用いて再帰的に定義される関数型プログラムとその項書き換えによる評価の考え方を説明
その後、関数型プログラムの理論的基礎となるλ計算の説明
●第３章プログラム図式の理論
Ｙａｎｏｖのプログラム図式と同じ記述能力を持つ単純プログラム図式とその性質の説明
その後、プログラム図式の代数的表現法を説明
●第４章プログラミング言語の構造的操作的意味論
プログラミング言語の抽象的構文定義法の説明
その後、プログラミング言語の構造的操作的意味論について説明
●第５章プログラミング言語の表示的意味論
領域理論と呼ばれる意味領域の数学的理論の概要を説明
その後、領域理論に基づく表示的意味論の説明、表示的意味論によるプログラムの性質の証明を支援する推論システムＬＣＦの基礎となる多相型λ計算ＰＰλの説明をする
●第６章プログラミング言語の公理的意味論
前提条件Ｐと帰結条件Ｑに関する文Ｓの弱正当性検証文を用いた論理的意味論の説明
●第７章正当性検証文に基くプログラム論理体系
強正当性検証文とそれを妥当にする最弱前提条件を手続き型プログラムと関数型プログラムの場合について定義し、強正当性にかんする構成的論理体系を与える
関数型プログラムの型推論が強正当性のための構成的論理体系の一例として扱えることを説明
If you enjoyed this article, please consider sharing it!
