{"created":"2023-06-19T09:51:07.598645+00:00","id":8152,"links":{},"metadata":{"_buckets":{"deposit":"0521a84d-7945-45fd-85eb-937e468f2089"},"_deposit":{"created_by":3,"id":"8152","owners":[3],"pid":{"revision_id":0,"type":"depid","value":"8152"},"status":"published"},"_oai":{"id":"oai:fukuyama-u.repo.nii.ac.jp:00008152","sets":["502:505:675:711"]},"author_link":["43765","43763","43764"],"item_1_biblio_info_14":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2003-12","bibliographicIssueDateType":"Issued"},"bibliographicPageEnd":"232","bibliographicPageStart":"225","bibliographicVolumeNumber":"27","bibliographic_titles":[{"bibliographic_title":"福山大学工学部紀要"}]}]},"item_1_creator_6":{"attribute_name":"著者名(日)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"石川, 洋"}],"nameIdentifiers":[{"nameIdentifier":"43763","nameIdentifierScheme":"WEKO"}]}]},"item_1_description_1":{"attribute_name":"ページ属性","attribute_value_mlt":[{"subitem_description":"P(論文)","subitem_description_type":"Other"}]},"item_1_description_12":{"attribute_name":"抄録(英)","attribute_value_mlt":[{"subitem_description":"We presents an approach to reason about specifications written in a formal specification language automatically. Our reasoning approach is based as follows: (1)Specifications are written in Z, one of formal specification languages. (2)Reasoning system is based on W, a logic for the Z notation. (3)Verification system is written using CafeOBJ. The logic W is similar to a sequent calculus in the style of Gentzen. CafeOBJ is an executable algebraic specification language. Therefore our approach attempts to transform the specifications into sequents. This paper gives an example how to translate the Z. notations into sequents and how to prove using them.","subitem_description_type":"Other"}]},"item_1_full_name_7":{"attribute_name":"著者名よみ","attribute_value_mlt":[{"nameIdentifiers":[{"nameIdentifier":"43764","nameIdentifierScheme":"WEKO"}],"names":[{"name":"イシカワ, ヒロシ"}]}]},"item_1_full_name_8":{"attribute_name":"著者名(英)","attribute_value_mlt":[{"nameIdentifiers":[{"nameIdentifier":"43765","nameIdentifierScheme":"WEKO"}],"names":[{"name":"ISHIKAWA, Hiroshi","nameLang":"en"}]}]},"item_1_source_id_13":{"attribute_name":"雑誌書誌ID","attribute_value_mlt":[{"subitem_source_identifier":"AN00217655","subitem_source_identifier_type":"NCID"}]},"item_1_text_10":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_language":"en","subitem_text_value":"Department of Information Processing Engineering, Faculty of Engineering, Fukuyama University"}]},"item_1_text_9":{"attribute_name":"著者所属(日)","attribute_value_mlt":[{"subitem_text_value":"福山大学工学部情報処理工学科"}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2003-12-01"}],"displaytype":"detail","filename":"KJ00005781548.pdf","filesize":[{"value":"736.1 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"url":"https://fukuyama-u.repo.nii.ac.jp/record/8152/files/KJ00005781548.pdf"},"version_id":"ed6d1c6c-296c-4c16-a006-bddb68397f22"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"形式仕様","subitem_subject_scheme":"Other"},{"subitem_subject":"Z","subitem_subject_scheme":"Other"},{"subitem_subject":"代数仕様言語","subitem_subject_scheme":"Other"},{"subitem_subject":"検証","subitem_subject_scheme":"Other"},{"subitem_subject":"Formal Specification","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Z","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Algebraic Specification Language","subitem_subject_language":"en","subitem_subject_scheme":"Other"},{"subitem_subject":"Verification","subitem_subject_language":"en","subitem_subject_scheme":"Other"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"departmental bulletin paper","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"形式仕様記述に基づく検証の自動化","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"形式仕様記述に基づく検証の自動化"},{"subitem_title":"On an Automatic Verification based on Formal Specifications","subitem_title_language":"en"}]},"item_type_id":"1","owner":"3","path":["711"],"pubdate":{"attribute_name":"公開日","attribute_value":"2003-12-01"},"publish_date":"2003-12-01","publish_status":"0","recid":"8152","relation_version_is_last":true,"title":["形式仕様記述に基づく検証の自動化"],"weko_creator_id":"3","weko_shared_id":-1},"updated":"2023-06-19T10:29:32.747563+00:00"}