ソフトウェアの形式的洗練化と検証に関する基礎的研究 Fundamental Studies on Formal Refinement and Verification for Software

この論文をさがす

著者

    • 林, 雄二 ハヤシ, ユウジ

書誌事項

タイトル

ソフトウェアの形式的洗練化と検証に関する基礎的研究

タイトル別名

Fundamental Studies on Formal Refinement and Verification for Software

著者名

林, 雄二

著者別名

ハヤシ, ユウジ

学位授与大学

北海道大学

取得学位

博士 (工学)

学位授与番号

乙第5619号

学位授与年月日

2000-03-24

注記・抄録

博士論文

140p.

Hokkaido University(北海道大学). 博士(工学)

目次

  1. 目次 / (0003.jp2)
  2. 1 はじめに / p1 (0004.jp2)
  3. 2 ソフトウエア開発方法論の課題 / p6 (0007.jp2)
  4. 2.1 プログラムとアルゴリズムの分析 / p6 (0007.jp2)
  5. 2.2 ソフトウエア開発方法論 / p10 (0009.jp2)
  6. 2.3 ソフトウエアに対する形式化 / p11 (0009.jp2)
  7. 2.4 システムの分類と抽象化 / p13 (0010.jp2)
  8. 3 仕様記述言語Zと洗練化 / p16 (0012.jp2)
  9. 3.1 形式的仕様記述 / p16 (0012.jp2)
  10. 3.2 Zの概要 / p17 (0012.jp2)
  11. 3.3 洗練化計算(Refinement Calculus) / p19 (0013.jp2)
  12. 4 IO正則式の形式的仕様への適用 / p23 (0015.jp2)
  13. 4.1 IO正則式 / p23 (0015.jp2)
  14. 4.2 従来からの洗練化との比較 / p26 (0017.jp2)
  15. 4.3 Z上のIO正則式の性質 / p27 (0017.jp2)
  16. 4.4 IO正則式の下での洗練化 / p34 (0021.jp2)
  17. 4.5 洗練化の例 / p37 (0022.jp2)
  18. 4.6 IO正則式に基づく洗練化手法の評価 / p48 (0028.jp2)
  19. 5 IO正則式に対するプログラム検証 / p50 (0029.jp2)
  20. 5.1 動的性を盛り込んだ仕様としてのIO正則式 / p50 (0029.jp2)
  21. 5.2 Zによる仕様の問題点 / p51 (0029.jp2)
  22. 5.3 Whileプログラム / p54 (0031.jp2)
  23. 5.4 IO正則式に基づいた証明の規則 / p56 (0032.jp2)
  24. 5.5 証明の例 / p61 (0034.jp2)
  25. 5.6 IO正則式に対するプログラム検証の評価 / p71 (0039.jp2)
  26. 6 データフローネットワークの分析 / p72 (0040.jp2)
  27. 6.1 データフローネットワークによるモデル / p72 (0040.jp2)
  28. 6.2 データフローネットワークにおける不動点 / p73 (0040.jp2)
  29. 6.3 表記法の定義 / p76 (0042.jp2)
  30. 6.4 基本プロセス / p77 (0042.jp2)
  31. 6.5 決定性データフローネットワーク / p85 (0046.jp2)
  32. 6.6 ネットワークの実行例 / p89 (0048.jp2)
  33. 6.7 最小不動点の考察 / p92 (0050.jp2)
  34. 6.8 不動点の解釈についてのまとめ / p97 (0052.jp2)
  35. 7 IO正則表現によるデータフローネットワークの検証 / p99 (0053.jp2)
  36. 7.1 データフローネットワークの性質 / p99 (0053.jp2)
  37. 7.2 プロセスに対するIO正則式 / p100 (0054.jp2)
  38. 7.3 IO正則式の意味 / p104 (0056.jp2)
  39. 7.4 実行条件集合と決定性 / p111 (0059.jp2)
  40. 7.5 ストリーム代入の意味 / p115 (0061.jp2)
  41. 7.6 ネットワークの検証 / p121 (0064.jp2)
  42. 7.7 ネットワークに対する検証の例 / p125 (0066.jp2)
  43. 7.8 10正則式による検証の評価 / p130 (0069.jp2)
  44. 8 おわりに / p132 (0070.jp2)
  45. 参考文献 / p136 (0072.jp2)
0アクセス

各種コード

  • NII論文ID(NAID)
    500000189724
  • NII著者ID(NRID)
    • 8000000190007
  • DOI(NDL)
  • 本文言語コード
    • jpn
  • NDL書誌ID
    • 000000354038
  • データ提供元
    • 機関リポジトリ
    • NDL ONLINE
    • NDLデジタルコレクション
ページトップへ