ソフトウェア工学(講義)はいいぞ

こんにちは.M2のまえけんです.

これは琉大情報工学科(知能情報コース )Advent Calendar 2018の2日目の記事です.

(割とローカルの話しとか学部生向けな話しとかが多いですがご容赦ください!)

 

今回は弊学科の選択講義の1つであるソフトウェア工学について書きます.

ソフトウェア工学とは

そもそもソフトウェア工学の意味についてwikipediaを見ると

ソフトウェア工学はソフトウェアの開発・運用・保守に関して体系的・定量的にその応用を考察する分野である

つまり良い感じにソフトウェアを開発していくぜって事なんだと思います多分.

この”良い感じ”というのはいろんな意味があると思うのですが,その中の1つに信頼性を高めるというのがあります.ソフトウェア(プログラム)はただ書いただけではダメで,そもそも正しく動くのかどうかを検証しないといけません.例えばプログラミング1の課題のプログラムを書いた時に正しく動くか確かめてからレポートを提出しますよね(FizzzBuzzだったら3入れたらちゃんとFizzが返ってくるかどうか確かめる,とか).

このように,入力を入れて期待する出力が返ってくるか確かめるのをテストと言います.テストをするツールにはRSpecとかありますね.

ソフトウェア工学(講義)

テストは世の中で普通に行われている手法ですが,世の中にはちゃんとプログラムが動くことを証明する方法があります.ソフトウェア工学という講義は,その証明とその方法について学ぶ講義です.講義ページはここから見れます.

講義はでは関数型言語のHaskellと定理証明支援システムのAgdaを主に使います.他には自然演繹という証明手法や圏論やMonadについてもやります.盛りだくさん.

この講義,結構難しい印象があるみたいです.たしかに,いきなり関数型言語やるし定理証明支援システムもまだ世の中で全然使われてないしあまり情報出てこないんですよね….

が,それでもこの講義を受ける意義はあると思います.

1. 言語自体の知識が深まる

弊学科では,2018現在のカリキュラムではPython, Java, C, とかについて学びますがどれもパラダイムはオブジェクト指向(手続き型)なんですよね.

対してHaskellは関数型というパラダイムなので,今まで学んだ言語と書き方も考え方もぜんぜん違います.例えば,変数が無い,voidが無い,forが無い,等.

それでプログラム書けるんか?と思うんですが書けるんです.すごい.例としてクイックソートのPythonとHaskellの実装例を見てみます.

Python

def quick_sort(arr):
    left = []
    right = []
    if len(arr) <= 1:
        return arr
    ref = arr[0]
    ref_count = 0
    for ele in arr:
        if ele < ref:
            left.append(ele)
        elif ele > ref:
            right.append(ele)
        else:
            ref_count += 1
    left = quick_sort(left)
    right = quick_sort(right)
    return left + [ref] * ref_count + right

 

Haskell

qsort []     = []
qsort (p:xs) = qsort lt ++ [p] ++ qsort gteq
                 where
                   lt   = [x | x <- xs, x < p]
                   gteq = [x | x <- xs, x >= p]

 

Haskellの方が行数も少ないし宣言的ですね.関数型言語を学ぶことで,今まで当たり前にできてたことについての知識が深まります.対比するとそれぞれの理解が深まる感じですね.

また,Haskellは型システムが強いので,プログラムの実行前(コンパイルの時点)にバグを見つけることができます.これも信頼性という意味では強力なシステムになってます.

さらに,Haskellは後述するAgdaと深い関わりがあります.

2. 証明が楽しい

(数学好きな人向けなんですが)証明って例えば三平方の定理の証明とか三段論法とかありますが,そういうのを考えるのって楽しいですよね.しかもそういう証明を計算機で解けてしまうというのが,数学と情報工学が合わさった感じがして楽しいです.

この講義では三平方の定理の証明とかはやらないんですが,三段論法とか出てくる命題論理をやります.(人間は動物,動物は死ぬ,それなら人間は死ぬ,とか)

これらの証明にはまず自然演繹で証明して,Agdaを使って計算機に実行させます.証明が正しければ正常終了,間違いであればエラー終了.

この命題と自然演繹での命題の操作は,実はプログラムの型や関数に対応させることができます.具体的にどう書くのかは…講義ページ見たり受けたりしてみてください(余白が足りない)

 

ということでソフトウェア工学(講義)の紹介でした.マジでハマる人にはハマると思うので,この記事みて興味出てきたら是非受けてみてください(たしか学部3年生向けだったかな)

で,この講義の評価は課題で決まるのですが,レポート少し難しいんですよね…

そんなあなたに!課題解答例をここで公開しているので見てみてください.(ただしAgdaの解答以外!そのうち載せる)(しかも毎年問題少し変わるので注意)

githubで公開しているので間違いとかあったらPRください.

さらに興味を持った人は学科slackの #ie-functionalを覗いてみてください.たまーーーーに関数型な勉強会をしてます.

 

以上まえけんでした.3日目はmayutsunaさんです.

Leave a Reply

You must be logged in to post a comment.