並行論理型プログラミング言語における段階的プログラム記述の検証

書誌事項

タイトル別名
  • Formal Verification for Stepwise Programming in Concurrent Logic Language

この論文をさがす

説明

本稿では,並行論理型プログラミング言語GHCについて,プログラムを有限集合に対応づける新しい意味論を構成する.これは,ある有限集合とそれを無限集合へと展開する演算によってなされる.また本稿ではこの意味論について,プログラムの意味をプログラムの仕様,意味写像をプログラムからプログラムの仕様を抽出する手続きと捉える.そしてこの意味論をラピッドプロトタイピングのような段階的プログラム記述おける形式的な検証に応用する.すなわち意味写像によって改変前のプログラムから仕様を組織的に生成し,改変後のプログラムがこれを満足するかを検証することで,プログラムの機能継承についての形式的な検証の手段とする.

収録刊行物

詳細情報 詳細情報について

  • CRID
    1571698602147506688
  • NII論文ID
    110002929442
  • NII書誌ID
    AN10464060
  • 本文言語コード
    ja
  • データソース種別
    • CiNii Articles

問題の指摘

ページトップへ