著者

大久保 徹似 二階堂 建人 丹羽 直也 高田 眞吾

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.33, no.2, pp.2_3-2_7, 2016-04-22 (Released:2016-06-22)

著者

権藤 克彦 新山 祐介 荒堀 喜貴

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.39, no.4, pp.4_97-4_128, 2022-10-25 (Released:2022-11-22)

---

本論文ではSwift言語のARC機能により発生する強い循環参照やメモリリークを自動的に検知する新しいツールUCDetectorを提案する.Swift言語の「静的型付けで安全な言語でありながら低レベルなプログラミングが可能」という特徴,SwiftリフレクションAPI,デバッガ lldb Pyton APIを用いることで,簡易かつコンパクトな実装が可能だったこと,その際に自明ではない様々な障壁があったことを知見として本論文では報告する.また,実装した循環参照検知器の精度と効率に対する予備評価の結果も報告する.

著者

古澤 仁 高井 利憲

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.23, no.3, pp.3_14-3_34, 2006 (Released:2006-09-30)

---

クリーニ代数は正規言語を公理的に取り扱うための代数的枠組みである.正規表現が計算機科学のいたるところに現れることを考えると,クリーニ代数が計算機科学に現れる構造の自然なクラスの性質を公理的にとらえ得るであろうことが容易に推測されるであろう.クリーニ代数の定義は,等式とホーン節で与えられるため,ある現象をクリーニ代数においてモデル化すると,その現象が簡単な式変形によって検証できるという特徴をもつ.本稿ではクリーニ代数の基本的な性質とそのプログラム理論への応用例について紹介する.

著者

梅村 晃広

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.27, no.3, pp.3_24-3_35, 2010-07-27 (Released:2010-09-27)

被引用文献数

1

---

本解説記事では,各種フォーマルメソッドの背後で動作する証明(補助)エンジンとしても注目を集めている,SATソルバ,SMTソルバについて,その背景,基本的な概念,技術動向および応用についての動向を解説する.SATソルバは近年飛躍的な技術革新があり,これに伴ない,いろいろな分野から応用への注目が集まるようになった.また,これに合わせるようにSMTソルバという発展的な概念も発生してきた.本稿は,これらについて,特にフォーマルメソッドとの関係における位置付けを概説するものである.

著者

藤田 憲悦

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.20, no.3, pp.285-291, 2003-05-23 (Released:2012-08-20)

---

カリー・ハワード同型を古典論理にまで拡張することにより,M.Parigotは古典論理の証明項を表現する体系としてλμ計算を導入した.本論文では,万能的な計算モデルの観点から,タイプフリーのλμ計算でもD. Scott流の外延的モデルが存在することを示す.そのために,(η)規則も妥当とするCPS変換を導入する.そして,D × D ≅ D ≅ [D → D]を満たす任意の領域Dから外延的λμモデルを構成する.さらに,合流性やC-monoidsとの興味深い関係についても論じる.

著者

松原 正樹 深山 覚 奥村 健太 寺村 佳子 大村 英史 橋田 光代 北原 鉄朗

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.30, no.1, pp.1_101-1_118, 2013-01-25 (Released:2013-03-05)

---

本論文では創作過程の視点に基づいて自動音楽生成に関するサーベイを行う.Shneidermanの創作過程の枠組みによれば,創作過程はCollect, Relate, Create, Donateの4つのフェーズからなる.計算機システム,ユーザ,システム設計者の3者全体を1つのトータルシステムと捉えると,創作においてそれぞれの要素が4つのフェーズをどう分担するか考えることができる.我々は既存の自動作曲・自動編曲・演奏表情付けシステムに対してこの観点から分析を行った.分類結果より各システムにおける4つのフェーズの共通項や差異を比較することができるようになり,音楽生成研究の進むべき方向性を示すことができた.

著者

川島 英之

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.33, no.3, pp.3_44-3_49, 2016-07-25 (Released:2016-09-25)

---

データ基盤システムを役割で大別すると,SQL問合せ処理システムとトランザクション処理システムという2つのサブシステムに分けられる.従来型のデータベース管理システム(DBMS)はこれらを兼ね備えている.一方,性能向上のために,近年はサブシステム毎の高度化が行われている.本論文ではこれらに関する近年の動向を解説する.

著者

森畑 明昌

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.29, no.1, pp.1_147-1_158, 2012-01-26 (Released:2012-02-26)

被引用文献数

1

---

正規表現はスクリプト言語などで広く使われているが,既存の処理系の多くはバックトラックを用いてこのマッチング処理を実装しており,最悪時の効率が悪い.実用的な様々な拡張を加えた正規表現に対するマッチングアルゴリズム,特に,文字列置換等の用途で用いられる「部分マッチの取り出し」を行えるアルゴリズムが望まれる.本論文では多くの処理系で利用可能な「先読み・否定先読み」をもつ正規表現の有限状態オートマトンへの変換を示す.まず,先読み・否定先読みを持つ大きさmの正規表現を状態数O(22m)の決定的有限オートマトンに変換する手法を示す.次に,部分マッチの取り出しを扱うため,重み付き正規表現を議論する.そして先読み・否定先読みを持つ大きさmの重み付き正規表現を状態数O(22m)の重み付き非決定的有限オートマトンに変換する手法を示す.これらのオートマトンにより効率の良いマッチングを達成できる.

著者

新屋 良磨

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.36, no.4, pp.4_84-4_85, 2019-10-25 (Released:2019-12-25)

著者

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

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

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

著者

片山 卓也

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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.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予想やその解決の難しさ,そして,この課題にどのように挑んでいるかを具体的な研究例を紹介しながら解説する.