A Behavioral Specification of Imperative Programming Languages

スポンサーリンク

概要

• 論文の詳細を見る

• In this paper, we give a denotational semantics of imperative programming languages as a CafeOBJ behavioral specification. Since CafeOBJ is an executable algebraic specification language, not only execution of programs but also semi-automatic verification of programs properties can be done. We first describe an imperative programming language with integer and Boolean types, called IPL. Next we discuss about how to extend IPL, that is, IPL with user-defined types. We give a notion of equivalent programs, which is defined by using the notion of the behavioral equivalence of behavioral specifications. We show a sufficient condition for the equivalence relation of programs, which reduces the task to prove programs to be equivalent.

• 社団法人電子情報通信学会の論文
• 2006-06-01

著者

• 中村 正樹

  金沢大学理工学域電子情報学類

• 中村 正樹

  北陸先端科学技術大学院大学情報科学研究科

• WATANABE Masahiro

  Production Engineering Research Laboratory, Hitachi Ltd.

• NAKAMURA Masaki

  School of Information Science, Japan Advanced Institute of Science and Technology

• 中村 正樹

  金沢大学 理工学域 電子情報学類

• Futatsugi Kokichi

  Jaist Nomi‐shi Jpn

• Futatsugi Kokichi

  School Of Information Science Jaist

• Nakamura Masaki

  Kanazawa Univ. Kanazawa‐shi Jpn

• Nakamura Masaki

  School Of Electrical And Computer Engineering Kanazawa University

• Watanabe Masahiro

  Production Engineering Research Laboratory Hitachi Ltd.

• FUTATSUGI Kokichi

  School of Information Science

関連論文

• B-2 代数仕様言語CafeOBJにおけるモデル検査(プログラムの理論,B.ソフトウェア)
• AS-3-4 CSTソリューションコンペティション2010の概要 : マルチカーエレベータの最適制御(AS-3.コンカレントシステム理論の最近の発展とその応用,シンポジウムセッション)
• AS-3-3 代数仕様に基づく実時間システムの検証(AS-3.コンカレントシステム理論の最近の発展とその応用,シンポジウムセッション)
• OTS/CafeOBJ法に基づく並行システムの実装とテスト生成(コンカレントシステム,離散事象システム及び一般)
• CSTソリューションコンペティション2010--マルチカーエレベータの最適制御 (コンカレント工学)
• RB-003 An algebraic specification of message passing programming languages
• CafeOBJ入門(6) : 通信プロトコルの検証
• CafeOBJ入門(5) : 認証プロトコルの検証
• CafeOBJ入門(4) : 証明譜による検証法(エージェント)
• CafeOBJ入門(3) : 等式推論と項書換システム
• Maude : 書換え論理に基づく計算機言語および処理系(ソフトウェア紹介)
• CafeOBJ入門(2) : 構文と意味
• CafeOBJ入門(1) : 形式手法とCafeOBJ
• LA-008 実行可能な代数仕様の停止性証明について(モデル・アルゴリズム・プログラミング)
• モジュラーな代数仕様言語のための項書き換えシステム(システム検証の科学技術)
• OTS/CafeOBJからOTS/Maudeへの仕様変換の研究
• 項書き換えシステムにおける可簡約演算子とその応用
• 項書き換えシステムにおける可簡約演算子とその応用
• STSプロトコルの形式化と検証によるCafeOBJとCoqの比較
• B-036 代数仕様言語CafeOBJと証明支援系CoqによるSTSプロトコルの形式化と検証(B.ソフトウェア)
• B-034 隠蔽代数に基づく命令型プログラム言語の意味論の記述と検証(B.ソフトウェア)
• LA-005 項書換えシステムにおける可簡約演算子とその応用(A. モデル・アルゴリズム・プログラミング)
• B-1 代数仕様言語CafeOBJのための拡張可能な前処理系(プログラムの理論,B.ソフトウェア)
• User-defined on-demand matching
• 依存対を用いた文脈依存書換え系の停止性判定について
• 消去法による項書換え系の停止性判定について
• 依存対を用いた文脈依存書換え系の停止性判定について
• 消去法による項書換え系の停止性判定について
• OTS/CafeOBJ法における証明譜からのテスト生成
• State Machines as Inductive Types(Concurrent Systems)
• Shot Leveling and Focusing with Interferometry for Optical Lithography of Sub-Half-Micron LSI
• Proof Score Approach to Verification of Liveness Properties
• Analysis of membership sharing in digital subscription services
• Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
• A Specification Translation from Behavioral Specifications to Rewrite Specifications
• Argument filtering transformation
• 文脈依存書き換えの拡張
• CSTソリューションコンペティション2010 : マルチカーエレベータの最適制御(CSTソリューションコンペティション2010,コンカレントシステム及び一般)
• Accuracy Improvement of Shot Leveling and Focusing with Interferometry for Optical Lithography
• Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm(Concurrent Systems)
• A Behavioral Specification of Imperative Programming Languages
• Concurrent Reflective Computations in Rewriting Logic(Theory of Rewriting Systems and Its Applications)
• システムと信号処理サブソの新たな展開を目指して(システムと信号処理及び一般)
• システムと信号処理サブソの新たな展開を目指して(システムと信号処理及び一般)
• システムと信号処理サブソの新たな展開を目指して(システムと信号処理及び一般)
• システムと信号処理サブソの新たな展開を目指して(システムと信号処理及び一般)
• Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method
• Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support
• A Scenario-based Object-Oriented Modeling Method with Algebraic
• 在宅患者見守りのための周辺器具からの情報収集システムの構築 (ユビキタス・センサネットワーク)
• 在宅患者見守りのための周辺器具からの情報収集システムの構築 (アドホックネットワーク)
• Common-Path Double-Pass Optical Interferometry Using a Wire-Grid Polarizer as a Reference Mirror
• A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"
• 在宅患者見守りのための周辺器具からの情報収集システムの構築(行動認識,フレッシュマン・セッション,ユビキタス・センサネットワーク,ユビキタス・システム,アドホックネットワーク)
• B-19-17 臀部・足位置検出機能を持つ立ち上がり動作評価システムの試作(B-19.ユビキタス・センサネットワーク,一般セッション)
• B-19-16 在宅患者見守り支援システムの危険行動識別の基礎的評価(B-19.ユビキタス・センサネットワーク,一般セッション)
• K-042 在宅療養患者危険行動検知システムの開発(作業・理学療法のための福祉情報工学,K分野:教育工学・福祉工学・マルチメディア応用)
• 立ち上がり動作における支持基底面および重心可視化システム (イメージ・メディア・クオリティ)
• 立ち上がり動作における支持基底面および重心可視化システム (マルチメディア･仮想環境基礎)
• 立ち上がり動作における支持基底面および重心可視化システム (福祉情報工学)
• 立ち上がり動作における支持基底面および重心可視化システム (画像工学)
• 看護師向け指さし呼称確認システムの試作 (マルチメディア･仮想環境基礎)
• 看護師向け指さし呼称確認システムの試作 (福祉情報工学)
• 装着型センサを用いた高次脳機能障がい者の運転技能評価システムに関する研究 (福祉情報工学)
• 看護師向け指さし呼称確認システムの試作 (画像工学)
• 看護師向け指さし呼称確認システムの試作 (イメージ・メディア・クオリティ)
• 立ち上がり動作における支持基底面および重心可視化システム(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 立ち上がり動作における支持基底面および重心可視化システム(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 立ち上がり動作における支持基底面および重心可視化システム(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 看護師向け指さし呼称確認システムの試作(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 立ち上がり動作における支持基底面および重心可視化システム(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 看護師向け指さし呼称確認システムの試作(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 看護師向け指さし呼称確認システムの試作(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• 看護師向け指さし呼称確認システムの試作(リハビリ・看護,メディア・コミュニケーションの品質と福祉,及び一般)
• A Note on "On the Construction of Boolean Functions with Optimal Algebraic Immunity"
• From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ

もっと見る 閉じる

スポンサーリンク