著者

Xuping Huang Shunsuke Mochizuki Akira Fujita Katsunari Yoshioka

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.64, no.3, 2023-03-15

---

In recent years, malware-infected devices, such as Mirai, have been used to conduct impactful attacks like massive DDoS attacks. Internet Service Providers (ISPs) respond by sending security notifications to infected users, instructing them to remove the malware; however, there are no approaches to quantify or simulate the performance and effectiveness of the notification activities. In this paper, we propose a model of security notification by ISPs. In the proposed model, we simulate the security notification with composite parameters, indicating the nature of malware attacks such as persistence of malware, user response ratio, and notification efforts by ISPs, and then discuss their effectiveness. Moreover, we conduct a simulation based on the actual attack.------------------------------This is a preprint of an article intended for publication Journal ofInformation Processing(JIP). This preprint should not be cited. Thisarticle should be cited as: Journal of Information Processing Vol.31(2023) (online)DOI http://dx.doi.org/10.2197/ipsjjip.31.165------------------------------

著者

中西 渉

出版者

情報処理学会

雑誌

情報処理

巻号頁・発行日

vol.64, no.4, pp.174-178, 2023-03-15

---

筆者はDNCLでのプログラミング学習環境PyPENを開発し,授業にも用いてきた.大学入学共通テストはDNCLで出題されるであろう.しかし,授業はDNCLでなく一般に使用されている言語で行うのがよいと考える.実際,生徒へのアンケートでも授業の実習はDNCLよりもPythonを使うことを望んでいるという結果が得られた.PyPENなどの環境は入試の演習には有効だと思われるが,授業で用いるものではない.

著者

井上 創造 ロペズ ギヨーム

出版者

情報処理学会

雑誌

情報処理

巻号頁・発行日

vol.64, no.3, pp.146-148, 2023-02-15

---

今回私たちが主催したThe 4th ABC(Activity and Behavior Computing,行動とふるまいに関する国際会議)を,主催者の視点から報告する.著者のうち井上は,東ロンドン大学のAtiqur Rahman Ahad氏とともに実行委員長を,ロペズはアールト大学のStephan Sigg氏とともにプログラム委員長を務めた.

著者

中山 泰一 Yasuichi NAKAYAMA

出版者

情報処理学会

雑誌

情報処理

巻号頁・発行日

vol.64, no.2, pp.73, 2023-01-15

---

2018年に高等学校の新学習指導要領が告示され,情報科は情報の科学的な理解に重点を置き,「情報I」と「情報II」が開講されることとなった.同じく2018年に,2025年からの大学入学共通テストで「情報I」が出題される方向性が示されたことから,都道府県市の教育委員会での情報科教員の採用が促進されることとなった.しかしながら,情報科のみを担当する教員(情報科専任教員)が少ない問題がある.情報科専任教員は発展的内容を教える「情報Ⅱ」を開講するためにも必要である.大学における情報科教員の養成はされている.都道府県市の教育委員会には,積極的に教員採用をして,情報科専任教員を増やしていただきたい.

著者

石井 岳史 川上 直人 橋本 剛 池田 心

出版者

情報処理学会

雑誌

情報処理学会研究報告. GI, 研究報告ゲーム情報学 (ISSN:21888736)

巻号頁・発行日

vol.2019, no.19, pp.1-8, 2019-03-01

---

ボードゲーム『ガイスター』は6×6のボード上で青赤2種8つの駒を交互に動かし,「脱出」「青駒全取り」「赤駒全取られ」のいずれかを狙う,対戦相手の駒の色がわからない2人用不完全情報ゲームである.不完全情報ゲームであるという点から運が影響しやすいが,駒の動きから非公開駒の種類を予測するなど心理戦の要素も多い.本ゲームにおいて上達するためには終盤の駒の動かし方について学ぶことが重要である.そこで詰将棋のような『詰めガイスター問題』を提案,実際に生成し有効性の考察を行うことで.対戦相手がいなくても初心者がガイスターに触れ,学ぶことができる環境の提供を目指す.本研究では通常のガイスターのルールに則った一般問題と,対戦相手の一部の駒を公開することで実戦での駒の種類予測を反映するような一部公開問題の2種を提案・考察する.一般問題では限られた勝利条件の問題しか生成できず,直感的に解くことができる問題が多かった.一部公開問題では,一般問題では生成できなかった青駒全取り問題を生成でき,アンケートでも高い評価を得ることができた.

著者

大場 みち子

出版者

情報処理学会

雑誌

情報処理

巻号頁・発行日

vol.63, no.12, pp.675, 2022-11-15

---

本コラムでは情報分野を中心としたJABEE(日本技術者教育認定機構)の概要とコロナ禍でのJABEE審査と個人的な想いを述べる.JABEEは主に理工系分野の高等教育機関における分野別教育の質保証に取り組んでいる.本会アクレディテーション委員会は,JABEEに協力して,情報専門系教育プログラム(ソウル協定対応),電子情報通信・コンピュータ工学および関連の工学分野の教育プログラムの審査を担当している.コロナ禍では,オンラインでの審査が基本となった.コロナ前の状態には戻らないであろうが,個人的には,もう一度,ともに汗を流した審査団の仲間と深夜の乾杯の気持ちを分かち合いたい.

著者

岩本 宗大 大西 鮎美 寺田 努 塚本 昌彦

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.63, no.10, pp.1574-1582, 2022-10-15

---

フィールドホッケーは,スティックと硬球を使って行う世界的に人気のあるスポーツである.フィールドホッケーの動作の中で,チームメイトへのパスとして最も基本的で一般的に使われる動作のうちの1つにプッシュという動作がある.プッシュ動作中,スティックにボールが接触してからリリースされるまでスティックがボールと接触している距離が長いと強くて速いプッシュを打てる.しかし,初心者が自分でスティックの接触点を知覚することは難しい.本研究では,プッシュの技術向上のためにスティックにボールが接触する位置の移動経路をリアルタイムに聴覚フィードバックするシステムを提案する.提案システムは,圧力センサの接触位置に応じてピッチの異なるフィードバック音を圧電スピーカによりリアルタイムで発生させる.2カ月間行った評価実験の結果,スティック上のボールの移動経路の平均距離は,聴覚フィードバックを行ったほうが,行わなかった場合よりも有意に長くなった.これにより,提案システムによる聴覚フィードバックの有効性を確認した.

著者

小野 厚夫

出版者

情報処理学会

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.46, no.6, pp.612-616, 2005-06-15

---

情報は日本で作られた言葉で、1876年出版の酒井忠恕訳『佛國歩兵陣中要務實地演習軌典』に最初の用例があり、その原語はフランス語のrenseignementである。初期には情報と状報が併用されていたが、ほどなく情報に統一された。はじめは兵語として用いられていたが、日清、日露戦争の記事で新聞用語として定着し、一般化した。第二次世界大戦後は英語のinformationの日本語訳として用いられ、科学的に取り扱われるようになった。

著者

及川 大志 池田 心

出版者

情報処理学会

雑誌

ゲームプログラミングワークショップ2018論文集

巻号頁・発行日

no.2018, pp.175-182, 2018-11-09

---

近年ゲームAIの研究は対戦相手として強いAIのみならず,ゲームそのものを楽しくするために様々な役割を担うようになってきている.テトリスは落下型パズルゲームとして長年数多くのプレイヤから愛されているゲームであるが,近年,T-spinと呼ばれている技術の登場により戦略の幅が大きく広がった.一方でこの技術は初心者にとって難解であり,また練習するための環境が十分整っていない.そこで本研究ではこのT-spinを学ぶ上で補助となる「詰めテトリス問題」を自動で生成する手法,さらにその面白さと難しさを教師あり学習で推定する手法を提案した.現時点では1手詰めのみを扱っているが,その面白さ・難しさを5段階評価の0.4ポイント程度の誤差で推測することに成功した.

著者

ジョヨンジュン 岩崎 敦 神取 道宏 小原 一郎 横尾 真

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.53, no.11, pp.2445-2456, 2012-11-15

---

本論文では不完全私的観測付き繰返しゲームの均衡を分析するプログラムを提案する.不完全私的観測付き繰返しゲームは,プレイヤが相手の行動についてノイズを含むシグナルを観測し,そのシグナルを他のプレイヤは観測できないという特徴を持つ.こうしたゲームは人工知能や経済の分野において様々な適用領域を持つため,大きく注目されている.しかし,このゲームにおける均衡を求めるには,非常に複雑な統計的推論が必要になるため,従来難しい未解決問題として知られていた.近年,均衡における振舞いを有限状態オートマトン(finite state automaton,FSA)で記述し,部分観測可能マルコフ決定過程(partially observable Markov decision process,POMDP)の理論を用いることで,あるFSAが均衡を構成するかどうかを明らかにできることが示された.しかし,その具体的な実装方法や実際の問題へ適用するためのプログラムは提供されていない.そこで本論文ではまず,標準的なPOMDPソルバのラッパとなるプログラムを開発する.このプログラムでは私的観測付き繰返しゲームの記述とFSAを入力として,そのFSAが対称的均衡を構成するかどうかを自動的に確認できる.さらに,このプログラムを繰返し囚人のジレンマに適用し,k-期相互処罰(k-MP)と呼ぶ新しいFSAのクラスを発見した.k-MPにおけるプレイヤは,初めに協力し相手の裏切りを観測するとそれ以降自分も裏切るが,続けてk回裏切りを観測すると元に戻り協力する.このプログラムを用いて状態数3以下のFSAを全探索した結果,繰返しゲームにおける観測構造パラメータのいくらかの範囲で,2-MPが他の純粋戦略均衡より優れており,従来よく知られている均衡である無限期罰則のトリガ戦略(grim-trigger)よりも効率的,つまり高い平均利得を実現することが分かった.The present paper investigates repeated games with imperfect private monitoring, where each player privately receives a noisy observation (signal) of the opponent's action. Such games have been paid considerable attention in the AI and economics literature. Since players do not share common information in such a game, characterizing players' optimal behavior is substantially complex. As a result, identifying pure strategy equilibria in this class has been known as a hard open problem. Recently, Kandori and Obara (2010) showed that the theory of partially observable Markov decision processes (POMDP) can be applied to identify a class of equilibria where the equilibrium behavior can be described by a finite state automaton (FSA). However, they did not provide a practical method or a program to apply their general idea to actual problems. We first develop a program that acts as a wrapper of a standard POMDP solver, which takes a description of a repeated game with private monitoring and an FSA as inputs, and automatically checks whether the FSA constitutes a symmetric equilibrium. We apply our program to repeated Prisoner's dilemma and find a novel class of FSA, which we call k-period mutual punishment (k-MP). The k-MP starts with cooperation and defects after observing a defection. It restores cooperation after observing defections k-times in a row. Our program enables us to exhaustively search for all FSAs with at most three states, and we found that 2-MP beats all the other pure strategy equilibria with at most three states for some range of parameter values and it is more efficient in an equilibrium than the grim-trigger.

著者

吉田 友太 池田 心

出版者

情報処理学会

雑誌

情報処理学会研究報告. GI, ゲーム情報学 (ISSN:21888736)

巻号頁・発行日

vol.2020, no.23, pp.1-8, 2020-03-06

---

グラディウスなどに代表される 2Dシューティングゲーム(STG)は,プレイヤが自機を操作して敵や弾を回避しながら進めるゲームであり,その面白さや難易度は,敵の配置や攻撃パターンから構成されたステージに大きく依存する.それらは通常,"初見で攻略することは困難だが,繰り返し同じステージをプレイすることで攻略法が見つけることができる"ように,人手でデザインされる.一方で,毎回見たことのない新しいステージをプレイしたいと考えるプレイヤ層も存在し,ランダムなステージ生成にも需要がある.しかし,完全にランダムに生成してしまうと,難易度や面白さの観点から,人間がプレイするには不適当なステージばかりが生成されてしまう.そこで本研究では,それらに配慮したステージの自動生成システムの構築を目指した.生成手法は様々存在するが,我々は,遺伝的アルゴリズムによる最適化に,AI プレイヤによる評価を組み合わせた生成検査法を採用した.評価関数としては,AI プレイヤのクリア状況や,緊迫度を図るために無行動率などが一定範囲に入っているかのペナルティなども加えた.また,多様性の抑制のため,敵の群れをステージの最小要素とした.さらに,人間らしい挙動を行う AI プレイヤを用いることで,「AI プレイヤには簡単だが,人間には難しい」といった難易度の誤推定の防止を図った.得られたステージは,被験者実験によって,工夫を行わないものよりも難易度・面白さともに良い評価を得た.

著者

小倉 加奈代 松本 遥子 山内 賢幸 西本 一志

出版者

情報処理学会

雑誌

インタラクション2010論文集 (情報処理学会シンポジウムシリーズ)

巻号頁・発行日

vol.2010, no.4, pp.259-266, 2010-03-01

---

本稿では,流速が異なる複数の時間流を持つチャットシステム“Kairos Chat”を提案する.対面口頭での対話では,人は議論の本筋とは関係の無い逸脱発言を行うことにより,議論の円滑化を図っている.同時に,逸脱発言を急速に忘却することで,議論記憶を自然に精錬化している.これは,人が各発言を,その内容に応じて異なる主観的時間流上で扱っている結果と見ることができる.しかし,従来のチャットシステムでは,すべての発言を単一の時間流上で扱うため,議論記憶としての発言履歴上に逸脱発言が混在し,精錬化が行われない.そこでKairos Chat では,各発言を内容に応じて異なる流速の時間流上で扱うことを可能とすることにより,逸脱発言のしやすさと,自然な発言履歴の精錬化の両立を目指す.被験者実験の結果,ユーザは自然に流速の違いを活用し,逸脱発言を気軽に行うとともに,発言履歴の精錬化が部分的に実現されることがわかった.また,各時間流と対話スレッドの関係性についても調査し,対話スレッドの中の4 割の隣接ペアが異なる時間流をまたぐものであることも明らかとなった. : In this paper, we propose a novel chat system named "Kairos Chat" that has multiple streams of time whose velocities are different. In a face-to-face communication, people facilitate a discussion using digressions and, at the same time, they naturally organize memories of the discussion by quickly forgetting them. We can regard this phenomenon as that they handle each utterance on a different stream of time based on its contents. However, the ordinary chat systems handle all of the utterances on a single stream of time. Therefore, the digressions are mixed into a chat log and the log cannot be naturally organized. Kairos Chat allows the users to handle each utterance on the different stream of time so as to strike a good balance between easy digressing and natural organizing of the chat log From experimental results with subjects, we found that the subjects naturally utilize the different streams of time, they readily digress and the natural organizing of the chat log can be partially achieved. We also investigated the relations between the streams of time and conversation threads and found that half of the threads drift among the streams.

著者

吉村 祐紀 西本 一志

出版者

情報処理学会

雑誌

情報処理学会研究報告.GN, グループウェアとネットワークサービス (ISSN:21888744)

巻号頁・発行日

vol.2017, no.17, pp.1-7, 2017-03-03

---

各種パーティにおいて,「同じ相手との会話を終えられず,他の人々と会話ができない」,「自分から話しかけることができない」などの問題を抱えた気弱な参加者を対象として,会話を希望する相手に対して,その意向を匿名で緩やかに伝えることでコミュニケーションの機会形成を支援するメディア ShyQueue を構築した.中規模のパーティを想定した運用実験によって,本システムの基本的有効性を確認した. : In various parties, there are often timid participants who cannot talk to someone with whom they want to talk and who cannot change conversation partners because they cannot finish current conversations. To support such timid people, in this paper, we propose a communication opportunity formation media named "ShyQueue," which allows a timid participant to anonymously convey his/her intentions that he/she wants to talk with you. We hosted a party with tens of participants and tried ShyQueue at this party. As a result, we confirmed basic effectiveness of ShyQueue.

著者

大石康智 亀岡 弘和 持橋 大地 永野 秀尚 柏野 邦夫

出版者

情報処理学会

雑誌

研究報告音楽情報科学(MUS) (ISSN:09196072)

巻号頁・発行日

vol.2010, no.9, pp.1-8, 2010-07-21

被引用文献数

1

---

本報告では,歌声のF0動特性をノート単位で編集し,歌い方を多様に変形できる歌声合成インタフェースの実現を目指し,その動特性のモデリングとモデルパラメータ推定に関する新しい解法を提案する.F0動特性は線形2次系に従うと仮定し,その生成過程を完全に確率モデルとして表現する.そして,EM法に基づいて,効率的なモデルパラメータ最適化アルゴリズムを導出する.最終的に,推定された2次系の振動を制御するパラメータと各ノートの音高を表すパラメータを個別に操作し,生成されたF0系列に基づいて歌声音響信号を変形して合成する"Vocal Dynamics Controller"を実装する.We present a novel statistical model for dynamics of various singing behaviors, such as vibrato and overshoot, in a fundamental frequency (F0) sequence and develop a note-by-note editing and synthesizing interface for F0 dynamics. We develop a complete stochastic representation of the F0 dynamics based on a second-order linear system and propose a complete, efficient scheme for parameter estimation using the Expectation-Maximization (EM) algorithm. Finally, we synthesize the singing voice using the F0 sequence generated by manipulating model parameters individually which control the oscillation based on the second-order system and the pitch of each note.

著者

横林 博 菅沼 明 谷口 倫一郎

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.45, no.5, pp.1451-1459, 2004-05-15

被引用文献数

9

---

文章の推敲支援を行うツールは多数存在するが,その多くは推敲支援に役立つ情報を提示するのみである.それらの情報を用いれば推敲作業自体は楽になるが,文章をどのように書き換えるかは書き手自身が考える必要がある.我々の研究室では,本稿に先立って係り受け解析過程モデルを作成した.このモデルは係り受けの複雑さの指標を基に文の複雑さを判定し,係り受けの複雑な文を抽出することができる.しかしどのように書き換えれば文の複雑さが減るかについては何も提示しない.そこで,この指標が下がるように,構文情報のみを用いて文の書き換え候補を作成することを考えた.複雑さの指標が下がれば,その文は書き換える前よりも複雑さが減っているといえる.さらに,この書き換え候補による推敲支援方法について述べる.Many writing tools for Japanese documents only notice a point of improving a sentence to a writer. He has to consider by himself how to rewrite a text. Our laboratory has proposed the model which imitates human dependency analysis for a Japanese sentence. The model can extract a complex sentence based on the indicator of complex dependency. It does not notices, however, anything about the method of decreasing the complexity of the sentence. In this paper, we describe a generating method of candidates for rewriting based on the indicator. We apply, furthermore, the method to a writing tool.

著者

川上 直人 池田 心 石井 岳史 橋本 剛

出版者

情報処理学会

雑誌

情報処理学会研究報告. GI, ゲーム情報学 (ISSN:21888736)

巻号頁・発行日

vol.2020-GI-43, no.13, pp.1-8, 2020-03-06

---

世界的に親しまれているチェスと似たようなルールを持ちながら不完全要素のあるボードゲーム『ガイスター』では,駒を交互に動かし 3つある勝利条件のいずれかを目指す.ガイスターでは強い AI プレイヤの研究が盛んにおこなわれている一方,教育,楽しさを目的としたコンテンツ生成の研究もあり,2019年3月には『詰めガイスター問題』が発案された.詰めガイスター問題は,ガイスターにおいて確実に勝てる局面を問題化したものであり,終盤力を上げる教育的コンテンツとなっている.2019年11月には,逆向き生成法と証明数探索により19手問題が生成された.また,別アプローチとして後退解析によって得られた37手問題も紹介され,後退解析によって長手数問題を効率的に生成できるのではないかと考えられている.本研究では,駒数が少ない局面に限定し,『詰めガイスター問題』の後退解析をおこなった.結果,駒数が 2対2の場合において「一般問題」では勝ち191,992局面,負け514,214局面,引き分け654局面,最長勝ち19手,「公開問題」では,勝ち783,232 局面,負け402,822局面,引き分け227,666局面,最長勝ち37手になることを確認し,引き分けの存在を確認できた.また,先行研究で議論されていなかった,問題のカテゴリ分け,解の一意性について定義,実験をおこない,いくつかの知見を得た.

著者

佐藤 彰洋 福田 豊 和田 数字郎 中村 豊

出版者

情報処理学会

雑誌

デジタルプラクティス (ISSN:21884390)

巻号頁・発行日

vol.11, no.3, pp.624-635, 2020-07-15

---

国立大学法人において,サイバー攻撃によるセキュリティインシデントが多発している.その攻撃に抗するため,我々が属す九州工業大学情報基盤運用室では学外公開アドレス管理システムを構築した.本システムの特徴は,学外公開,すなわち学外から到達可能なIPアドレスを付与した機器に関する情報共有と,それに対する措置として脆弱性改善と通信制御を実現したことにある.その導入により,本学のネットワークにおいて高い堅牢性の実現を確認した.本稿では,学外公開アドレス管理システムの設計と,12カ月にわたるシステムの運用による有効性の評価,そこから得られた知見について報告する.

著者

松本 行弘

出版者

情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.2, no.2, pp.27-36, 2009-03-23

---

多くのスクリプト言語において多言語テキスト処理は Unicode を固定的な内部文字コードとして採用しているが,その場合,Unicode 以外の文字集合で表現されたテキストを処理するためには文字集合間の変換が必要になり,文字集合間の互換性や文字集合における歴史的な事情などによりさまざまな問題を引き起こす可能性がある.そこで筆者が開発しているスクリプト言語 Ruby に対して,固定的な内部文字集合を持たない文字集合独立方式を採用し,文字集合間の変換をできるだけ行わないテキスト処理機能を実装した.本論文で述べる Ruby の多言語テキスト処理機能は,Unicode を固定的な内部文字集合とする他スクリプト言語 (Perl および Python) と比べて,テキスト処理におけるプログラムの簡潔さおよび性能において劣らない実用的なものであることを示す.本論文で述べる多言語テキスト処理機能は Ruby バージョン 1.9 として公開されている.Many scripring languages of present days use Unicode as their universal internal character set to manipulate multilingual text processing. But due to character set compatibility and other historical issues, text conversion to/from the universal character set may cause various problems. We designed and implemented character set independent multilingual processing, which avoids character set conversion as much as possible. We show that multilingual text processing in Ruby is practical in both productivity and performance, comparing other scripting languages, e.g. Perl and Python. The work described in this paper is publicly available in Ruby version 1.9.

著者

金藤栄孝 二木厚吉

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.45, no.3, pp.770-784, 2004-03-15

被引用文献数

1

---

Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降,goto文の使用に関する問題は長く議論されてきたが,goto文の使用法に関しての理論的裏付けを持つ研究としては,逐次的プログラムの制御フローは3基本構造(順次接続,条件分岐,反復)のみで表現可能であるからgoto文を用いたプログラムは3基本構造のみによる等価なプログラムに書き換えられる,という結果に基づいたMillsらのgoto文排斥論以外は皆無であり,Dijkstra本来のプログラムの正しさを示す手段としてのプログラムの構造化という観点でのgoto文の使用の是非は,プログラム検証論の立場から考察されなかった.本論文では,プログラムの正しさを示すという検証手段としてのHoare論理に基づきgoto文の使用を再検討する.特に,多重ループの打ち切りの場合,goto文を用いて脱出するプログラミングスタイルの方が,Mills流のBoolean型変数を追加してループを打ち切るスタイルよりも,Hoare論理での証明アウトラインが簡単に構成でき,したがって,前者のgoto文を用いたプログラミングスタイルの方が,そのようなプログラムに対するHoare論理による検証上からは望ましいことを示す.There have been a vast amount of debates on the issue on usages of goto statements initiated by the famous Dijkstra's Letter to the Editor of CACM and his proposal of ``Structured Programming''.Except for the goto-less programming style by Mills based on the fact that any control flows of sequential programs can be expressed by the sequential composition, the conditional (If-Then-Else)and the indefinite loop (While), there have not been, however, any scientific accounts on this issuefrom the Dijkstra's own viewpoint of verifiability of programs.In this work, we reconsider this issue from the viewpoint of Hoare Logic,the most standard framework for proving the correctness of programs, and we see that usages of goto's in escaping from nested loops can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using a goto for this purpose is easier than constructing the proof-outline of a Mills-style program without goto by introducing a new Boolean variable.

著者

崔 雄 西浦 敬信 矢野 桂司

出版者

情報処理学会

雑誌

情報処理学会研究報告 (ISSN:18840930)

巻号頁・発行日

vol.2010, no.5, 2011-02