私たちの生活を便利にするソフトウェア。 そのエラーを防ぐために、「数理論理学」が活躍する!?

  • ようこそ、ゲストさん
  • ログイン
  • 会員登録(無料)
  • エリア設定
MENU
閉じる
  • ようこそ、ゲスト さん

    会員登録(無料)

  • 適学・適職診断無料!

    診断を受ける

  • エリア設定

現在4校がカートに入っています。

一度に最大30校までまとめて資料請求することができます。

閉じる

「マイナビ進学」サイトが別タブで開きます。

私たちの生活を便利にするソフトウェア。
そのエラーを防ぐために、「数理論理学」が活躍する!?

2020.03.01

提供:東邦大学

私たちの生活を便利にするソフトウェア。
そのエラーを防ぐために、「数理論理学」が活躍する!?

私たちの生活にもはや欠かせないものとなっている多種多様のコンピュータ。パソコンはもちろん、スマホや電子レンジなど、身の回りにある便利なもののほとんどがコンピュータを搭載していると言っても過言ではないでしょう。
さて、このコンピュータを定義するとき、ハードウェアとソフトウェアの2つの存在が欠かせません。人間でいうカラダの部分となるハードウェアに対し、脳みそに例えられるソフトウェア。私たちが快適に生活を送ることができているのは、このソフトウェアが正しく機能しているおかげなのです。

この記事をまとめると

  • 私たちの安全で便利な生活はコンピュータの”頭脳”にかかっている!
  • 「数理論理学」を学んでソフトウェアのエラーを防ぐ!
  • まだまだ未開拓な分野を研究して、未来を切り開こう!

スマホや自動改札、電子レンジにATM……ハードウェアだけでは何も成り立たない

すべてのコンピュータは、「箱」の役目であるハードウェアだけでは動きません。コンピュータを動かす頭脳であり司令塔であるソフトウェアが、プログラム通りにコンピュータを動かし、私たちの生活を大きく支えています。
例えば、電車に乗るときには交通系ICカードをタッチして改札を通りますし、冷たいものを温めたければ電子レンジを使いますよね。もちろんほとんどの人が肌身離さず持ち歩いている携帯電話やスマートフォンも同様です。私たちの目的通りにソフトウェアが作動するのは、すべてプログラムが正確に動いているからなのです。
改札口にICカードを当てると、乗車駅や乗り換えの情報が瞬時に判断されますが、このような情報も全てソフトウェアが処理しています。また、炊飯器や電子レンジ、銀行のATMや自動車なども、すべてソフトウェアのおかげで作動しています。機械(箱)の中でプログラムが正確に動かなければ、電子レンジもATMもICチップも何の役にも立ちません。このように、私たちの生活を便利にしてくれているさまざまなコンピュータにとって、ソフトウェアは必要不可欠な存在なのです。

ソフトウェアのエラーを防ぐためには「プログラム検証」が不可欠!

ソフトウェアが正常に動かなくなると、私たちの生活に大きな影響が出てしまいます。
例えば、スマートフォンのアプリが正しく起動しなかったり、自動改札機が開かない、電車や新幹線が動かない…など、機械が誤作動を起こしたり、停止してしまいます。プログラムの些細なミスによって、世の中の大きな混乱につながる恐れがあるのです。しかし、コンピュータプログラムを作っているのは私たち人間です。人の手でプログラムを打ち込むため、どうしてもミスは発生しかねません。
そんなミスを未然に防ぐために欠かせないのが、「プログラム検証」。これは、プログラムの性質を手動や自動で証明し、エラーを確実に防ぐ作業です。
検証方法は大きく分けて2つあり、実際にプログラムを動かしてみる「動的作動」と、プログラムが『仕様(プログラマの意図)通りであること』を数学的に証明し、保証する「静的動作」が存在します。そして、この「静的動作」でプログラム検証をする際に必要になるのが「数理論理学」という学問。「数理論理学」とは、高校で習う数学のように数式で「答え」を導き出すものとは少し異なっており、三段論法や背理法など様々な方程式を用いながら、人間の論理的思考を数学的手法により探究をしていきます。

近い未来、機械が自分でプログラム検証?東邦大学の学びに注目!

専門性と人間性を備えた研究者、科学技術者を育成する東邦大学の理学部。同学部の情報科学科では、この「数理論理学」を用いてソフトウェアの安全性向上を目指し、プログラム検証の技術開発に挑んでいます。
研究室では現在、「プログラム検証」の研究と「全自動ツール」を組み合わせ、“機械だけで検証作業が進められる”全自動ツールの開発を進めています。この研究により、現在は人間が手間暇をかけて繰り返している検証作業が、将来すべて機械で完結するようになるかもしれません。
また、プログラム検証の研究に加えて、プログラムを細かく分割してバグを発見できる「関数型プログラミング言語理論」や、多くのデータ型の階層を構築し、それぞれに数学的実体を割り当てる「型理論」など、このほかにも様々な研究が行われています。どちらも「全自動ツール」に通じる基礎研究であり、ソフトウェアの安全性向上を目指すために必要な技術です。
将来、私たちの生活はさらに発展し、より一層テクノロジーの発達が期待されます。プログラムの知識に長けた人材は、今後ますます求められるようになるでしょう。未来を動かすような研究分野にチャレンジして、一緒に未来を切り開きませんか?

【広告企画】提供 : 東邦大学

この記事のテーマ
情報学・通信」を解説

情報通信産業には、通信業、放送業、情報サービス業、インターネット付随サービス業、映像・音声・文字情報制作業の5分野があります。近年は各分野の垣根が取り払われつつありますが、なかでも注目されているのが、インターネットに代表されるコンピュータを介した情報通信工学でしょう。高度に情報化が進んだ現代において、安全保障や経済政策はもちろんのこと、日常生活に至るあらゆるシーンで必要とされる、活躍の場の広い学問です。

「情報学・通信」について詳しく見る

この記事で取り上げた
「情報学」
はこんな学問です

情報学という学問名で、文系と理系の2種類の学問を表す。文系学問としては、人文・社会科学系の学問と連携し、社会システムのなかでの情報技術の役割や、マスコミュニケーションにおいての情報メディアの役割、国境を越えての情報コミュニケーションを研究テーマとする。理系学問としては、コンピュータのハードウェアやソフトウェア、情報システムが稼働する原理など、情報についての基礎となる分野を数学的手法によって研究する。

「情報学」について詳しく見る

この記事のテーマ
数学・物理・化学」を解説

私たちの生活基盤である自然界で生じるさまざまな事象や物質、それらが織りなす理論が研究対象です。宇宙や生物がどのようにして誕生し、どのような構造になっているのかという、究極的な知的探究心は人類ならでは。森羅万象の構造や性質、法則と変化を探求する物理や化学、その習得に必要な数学というように、これらの学問は互いに深く関連しています。未知の領域への研究を進めながら、さまざまな原理解明をしていく分野です。

「数学・物理・化学」について詳しく見る

この記事で取り上げた
「数学」
はこんな学問です

高校で学ぶ数学をさらに深く追究したり、異なる視点から考えたりする学問。主要な分野としては、方程式で数の関係の成り立ちを表す「代数学」、図形などの性質を研究する「幾何学」、微積分に代表される「解析学」がある。また、これらとは違う視点で、数学を活用してさまざまな現象を数理モデルで表そうとする「応用数学」もある。コンピュータ技術との関わりも深いため、ますます重要性が増している分野である。

「数学」について詳しく見る

あなたの適性にあった学びや仕事が見つかる

適学・適職診断

無料

進学・適職診断を受ける