Formal Verification for Stepwise Programming in Concurrent Logic Language

Bibliographic Information

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

Search this article

Description

In this paper, we construct a new semantics for concurrent logic programming language GHC which maps a program to a finite set. We achieve that by a finite set and an operator which extends the set to an infinite one. We regard the semantics-mapping as a procedure to extract specifications of programs. We apply the semantics to the formal verification for stepwise programming such as rapid-prototyping. We present a method to verify whether the next version of a program inherits the functions of the original version using the specification generated from the original one by the semantics-mapping.

Journal

Details 詳細情報について

  • CRID
    1571698602147506688
  • NII Article ID
    110002929442
  • NII Book ID
    AN10464060
  • Text Lang
    ja
  • Data Source
    • CiNii Articles

Report a problem

Back to top