著者

加藤 弘之 胡 振江 日高 宗一郎 松田 一孝

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.31, no.2, pp.2_44-2_56, 2014-04-24 (Released:2014-06-24)

---

双方向変換とは,ソースデータをターゲットデータに変換した後,ターゲットデータ上の更新をソースデータに反映させることが可能な計算の枠組みのことである.双方向変換の考え方は,古くはデータベース分野におけるビュー更新問題として扱われてきたが,近年は新しいプログラミングモデルと進化的ソフトウエア開発の手法として注目を浴び,プログラミング言語の観点から様々な双方向変換言語が提案されてきた.この解説論文は,会話の形で,プログラミング言語,ソフトウェア工学,データベースの視点から,双方向変換の歴史,基本原理,実践,応用,そして今後の課題について概説する.

著者

桜川貴司 Takashi Sakuragawa 京都大学数理解析研究所

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.4, no.3, pp.15-27, 1987

被引用文献数

1

---

Temporal Logicに裁づいた論理型言語を紹介する.この言語によって,並列処理・待ち合わせ・相互排除・非決定性などを容易に表現できる.applicationとしてはexecutable specification languageとしての使用を念頭においている.

著者

島内 剛一

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.1, no.2, pp.183-188, 1984-07-13

著者

片山 卓也

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.36, no.3, pp.3_33-3_46, 2019-07-25 (Released:2019-09-25)

---

国民年金法の述語論理による記述と定理自動証明システムZ3Pyによる検証に関するケーススタディついて述べた.法令の作成は伝統的に人手により行われて来たが,近年法令が大量に作られるようになり,その品質の維持には計算機科学,特にソフトウェア工学や人工知能で培われた技術を応用することが有効であると考えられる.本稿では,法令を意図した通りに正しく作る上で,法令の形式的記述と自動検証技術が有効であることを確認する目的で,国民年金法の基本的条文の述語論理による記述と,そのSMTソルバーZ3Pyによる検証を試行した結果を報告する.法令の文章上の複雑さは別にすると,その論理的深度は深くなく,このような方法が誤りの無い法令を作る上で有効な方法になり得ることが分かった.

著者

川本 裕輔

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.4, pp.4_67-4_83, 2016-10-25 (Released:2017-01-14)

---

本論文では,暗号系の安全性を検証する方法について,暗号理論の初歩からコンピュータ上で安全性証明を書く最先端の研究までを解説する.暗号系の安全性は攻撃の確率や計算量を用いて定式化されるため,その数学的証明は煩雑であり,しばしば間違いも生じる.そこで,安全性証明を形式手法で記述し,証明の正しさをコンピュータ上で機械的に確かめる研究が盛んになっており,様々な検証ツールが開発されている.その中でも,検証ツールEasyCryptは,従来のツールよりも簡単に,厳密な安全性証明が得られる.本論文では,まず,確率的多項式時間チューリング機械の間のゲームとして暗号系の安全性を定式化し,ゲームの書き換えによって安全性を証明する手法を説明する.次に,確率関係ホーア論理を用いた安全性証明の形式化について述べ,検証ツールEasyCryptを用いて安全性証明を書く方法を紹介する.なお,本論文は暗号理論や定理証明支援系についての知識を仮定していない.

著者

高野 保真 岩崎 英哉 佐藤 重幸

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.32, no.1, pp.1_253-1_287, 2015-01-26 (Released:2015-02-11)

---

関数型言語 Haskellは,遅延評価を標準とするプログラミング言語であり,近年注目を集めている.デファクトスタンダードの処理系である Glasgow Haskell Compiler(GHC)は多くの研究の基盤として用いられ,新しい言語概念など先進的な研究成果が取り入れられている.その一方で,GHCの実装は巨大で複雑になってきており,GHCに新機能を導入することは障壁が高くなってしまった.このような状況において,我々は実行時メモリの効率化を目指して,遅延オブジェクトを再利用する手法を提案し,GHCに実装してきた.我々が提案した手法は,コンパイル時にプログラム変換を行い,再利用対象とする遅延オブジェクトへの参照を単一にした上で,遅延オブジェクトを破壊的に書き換えて再利用する.その基本的な機構は既に先行論文において述べ,メモリ削減の効果も確認済みである.本論文は,再利用手法を実現するために考えられる各種手法の実装方法,および,それらの手法の得失・取捨選択に関する議論を詳細に行う.また,再利用手法の基本的な機構の実装で培った経験を生かし実装した,再利用手法の改善技法をいくつか提案する.それらの技法を導入することにより,実行時間に関するオーバヘッドを低く抑えることが可能であることを実験により確認した.最後に,GHCを研究の基盤に用いた経験より得られた遅延型関数型言語処理系に関する知見についても述べる.特に,GHCが Haskellで記述されていることは,処理系の拡張性に大きく貢献していることが分かった.

著者

吉崎 航

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.28, no.4, pp.4_35-4_40, 2011-10-25 (Released:2011-12-25)

著者

山中 祥太 栗原 一貴 宮下 芳明

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.30, no.3, pp.3_53-3_63, 2013-07-25 (Released:2013-09-25)

---

視線計測技術の精度は年々向上しているものの,ユーザが操作したいと考えて注視している画面内のオブジェクトを視線情報のみから特定することは困難であると言われている.一方で,注視していない範囲は容易に特定できるため,この領域を適切に利用することで新たなインタラクションが可能になると考えた.本論文では,注視していない領域においてカーソルの移動速度を上昇させ,ポインティングを高速化する手法を提案する.評価実験では,PC操作において日常的に行われるアイコンクリックを想定したタスクを行い,選択時間とエラー率を計測した.実験に用いたカーソル速度は,OSの標準速度,OSの最高速度,提案手法の3種類である.実験の結果,提案手法は標準速度より選択時間が短縮され,かつエラー率は上昇しないことから有効性を示した.

著者

上野 乃毅

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.26, no.4, pp.4_30-4_38, 2009-10-27 (Released:2009-12-27)

---

ソフトウェアへの機能追加のために実装の大規模な刷新が必要になることがある.実装刷新において後方互換性を完全に保つのは難しく,作業の途中で頓挫する例が後を断たない.実装刷新に失敗すると,開発プロジェクトでは巻き戻しの作業が発生するだけでなく,実装刷新を担当した開発者がモチベーションを欠き,長期的な生産性低下に繋がる恐れがある.本論文では,オープンソース開発における実装刷新の失敗事例を調査し,共通の要因とその対処法を明らかにした.調査の有効性を示すために,世界中に膨大な数のユーザを抱えるソフトウェアGNU Emacsの暗号化サブシステム(約4500行)に関して,提案手法に従って刷新を行なったところ,作業を円滑に完遂できた.

著者

龍田 真

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.8, no.3, pp.210-216, 1991-05-15

著者

角谷 良彦

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.1, pp.1_167-1_179, 2008 (Released:2008-02-29)

---

本論文では,直観主義様相論理IKにCurry-Howard対応する名前呼び及び値呼びの計算系を提案する.名前呼び計算は,圏論的意味論に基づいており,単純型付き名前呼びλ-計算の拡張となっている.本論文は,名前呼び計算の簡約系が強正規化可能性及び合流性を持つことを証明する.また,値呼び計算は,値呼びのλ-計算として定評のあるλc-計算の拡張として定義される.名前呼びの場合と同様,値呼び計算に対しても簡約系を与え,その強正規化可能性及び合流性を証明する.加えて,本論文では,値呼び計算の部分体系が名前呼び計算へのCPS変換によって特徴付けられることを示す.最後に,様相論理IS4への計算系の拡張についても考察する.

著者

伊藤 貴之

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.34, no.1, pp.1_94-1_95, 2017-01-25 (Released:2017-03-25)

著者

新屋 良磨 山口 勇太郎 中村 誠希

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.40, no.2, pp.2_49-2_60, 2023-04-21 (Released:2023-06-21)

---

言語Lが正規可測であるとは,Lに「収束」する正規言語の対の無限列が存在することを言う.本論文では,正規言語の代わりに正規言語の部分クラスである区分検査可能(Piecewise Testable (PT): 部分語の出現情報の Bool 演算で記述可能)言語および文字検査可能(Alphabet Testable (AT): 文字の出現情報の Bool 演算で記述可能)言語に焦点を当てその可測性を考察する.特に,正規言語に対するAT可測性はco-NP完全である一方,PT可測性は線形時間で決定できることを示す.

著者

渡辺 治

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.2, pp.2_33-2_40, 2012-04-25 (Released:2012-06-25)

---

計算複雑さの理論の研究についての解説.計算複雑さの理論は計算機科学の一分野であり,ソフトウェアの基盤であるアルゴリズムの設計の基礎理論でもある.しかし,ソフトウェアの開発などからは少し離れた研究分野でもある.この解説では,この近くて遠い計算複雑さの理論に親しみを持って頂くために,この分野の研究者たちは日々どんな研究をしているのか,という観点からの紹介を試みる.計算複雑さを研究する意義,この分野の重要なテーマであるP ≠ NP予想やその解決の難しさ,そして,この課題にどのように挑んでいるかを具体的な研究例を紹介しながら解説する.

著者

大和田 茂

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.23, no.4, pp.4_47-4_50, 2006 (Released:2007-06-11)

---

我々は,形状をゼリーの内部にプリントするゼリープリンターを提案する.このプリンターでは,出力形状が柔らかいゼリーであるために,加工が非常に容易であることが大きな利点としてあげられる.これにより,コンピュータの内部の情報を実世界に取り出し,変形したり加工したり食用にすることが可能となる.さらに,三次元の標高データを出力することもできるので,自由に切ってその断面をみることも可能である.

著者

横尾 真 岩崎 敦 櫻井 祐子 岡本 吉央

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.4, pp.4_15-4_31, 2012-10-25 (Released:2012-12-25)

---

本稿では,メカニズムデザイン(基礎編)として,メカニズムデザイン理論について概説する.メカニズムデザイン理論は不完備情報ゲームの枠組みを用いて,自身の利得の最大化を目指して行動するプレイヤの集団が,あるルール(メカニズム)の元でどのように振る舞うかを分析すると共に,どのようにメカニズムを設計すれば社会的に望ましい結果,もしくは設計者の目的を満たす結果を達成できるかを扱う理論である.本稿では,まずメカニズムデザインの基礎となる不完備情報ゲームを説明する.そして,メカニズムデザインの代表的な適用例であるオークションに即して,メカニズムデザインの考え方,およびただ1つの商品を販売するオークションにおけるメカニズムデザイン理論の主要結果を概説する.

著者

横尾 真 岩崎 敦 櫻井 祐子 岡本 吉央

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.2, pp.2_69-2_84, 2012-04-25 (Released:2012-06-25)

---

本稿では,ゲーム理論の基礎となる標準形の非協力ゲームについて概説する.標準形の非協力ゲームでは,複数のプレイヤが,自身の利得の最大化を目指して,独立かつ同時に行動を選択する.各プレイヤの利得は,自身の行動と他のプレイヤの行動の組合せにより決定される.非協力ゲームの帰結を予測するために,様々な均衡概念が提案されている.本稿では,標準形の非協力ゲームの基礎となる用語と均衡概念について概説する.また,単純に標準形の非協力ゲームを記述した場合,その記述量はプレイヤの数に対して指数的に増加する.本編では,ゲームの簡潔な記述方法であるグラフィカルゲームと混雑ゲーム,およびこれらのゲームにおいて均衡を計算するためのアルゴリズム/計算量について概説する.

著者

石尾 隆

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.1, pp.1_47-1_60, 2012-01-26 (Released:2012-03-26)

---

動的解析とは,プログラムの実行時情報を収集し,その実際の振舞いや性能を解析するための技術である.本稿では,ソースコードに対する解析と比べた場合の動的解析の特徴を述べ,コードカバレッジの計算や統計的デバッギングなどの動的解析手法を解説する.また,読者が解析手法を試すことができるように,Javaプログラムの解析に役立つツールについても紹介する.

著者

肥後 芳樹 吉田 則裕

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.28, no.4, pp.4_43-4_56, 2011-10-25 (Released:2011-12-25)

---

コードクローンとは,ソースコード中に存在する互いに一致,もしくは類似したコード片を指す.コードクローンの存在は,ソフトウェアの開発および保守に悪影響を与える恐れがあるといわれている.本稿では,コードクローンを取り除くためのリファクタリング方法と近年の研究成果について紹介する.

著者

佐々 政孝

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.2, no.3, pp.3_560-3_562, 1985-07-15 (Released:2018-11-05)