|
JAIST Repository >
School of Information Science >
JAIST Research Reports >
Research Report - School of Information Science ： ISSN 0918-7553 >
IS-RR-2015 >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/10119/12607
|
| Title: | Generic Proof Scores for Generate & Check Method in CafeOBJ |
| Authors: | Futatsugi, Kokichi |
| Issue Date: | 2015-02-18 |
| Publisher: | 北陸先端科学技術大学院大学情報科学研究科 |
| Magazine name: | Research report (School of Information Science, Japan Advanced Institute of Science and Technology) |
| Volume: | IS-RR-2015-002 |
| Start page: | 1 |
| End page: | 32 |
| Abstract: | Generic proof scores for the generate & check method in CafeOBJ are described. The generic proof scores codify the generate & check method as parameterized modules in the CafeOBJ language independently of specific systems to which the method applies. Proof scores for a specific system can be obtained by substituting the parameter modules of the parameterized modules with the specification modules of the specific system. The effectiveness of the generic proof scores is demonstrated by applying them to a simple but non-trivial example. |
| URI: | http://hdl.handle.net/10119/12607 |
| Material Type: | publisher |
| Appears in Collections: | IS-RR-2015
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| IS-RR-2015-002.pdf | | 237Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
