もし C# で形式的検証ができたら

C# では、コンパイル時に静的にコードをチェックし、警告やエラーを通知してくれます。
例えば、次のようなものです。

到達できないコード

ジェネリック型制約

1 つ目の例はステートメントの条件分岐により、そのスコープに到達できるかどうかを判定しています。
実行はでき、致命的ではないため、エラーではなく警告が通知されています。
2 つ目の例の where 句では、ジェネリック型に対する制約が指定されています。

現時点のコンパイラもそれなりに強力な判断能力を持っているとは思いますが、
もし C# のコンパイラがさらに空気を読んで賢くなったら、
どのようなプログラミング エクスペリエンスを実現できるのかを考えてみましょう。

実装のお題として「与えられた 2 つの整数を昇順に並べ替えるメソッド」という単純なものを設定し、
どうすればバグのないプログラミングができるかを考えます。

まず、並べ替えのメソッドが満たすべき条件は次の通りです。

  1. 実行結果が意図した順番に並んでいる
  2. 実行前の値のセットと実行後の値のセットが同じである

そこで、メソッドの実装を始める前に、メソッドのシグネチャでこれらの条件を表現してみます。

Program.cs


/*
* このプログラムには、架空の機能が含まれます。
*/
class Program
{
    static void Main(string[] args)
    {
        var sorted = Sort(new TwoValues(2, 1));
    }

    // (架空の機能) 引数に対する高度な制約。
    static OrderedTwoValues Sort(TwoValues v) where Sort(v).SetEquals(v)
    {
        // TODO: あとで実装。
        throw new NotImplementedException();
    }
}

// (架空の機能) null を代入できない型。
public class TwoValues where this != null
{
    public int X { get; private set; }
    public int Y { get; private set; }

    public TwoValues(int x, int y)
    {
        X = x;
        Y = y;
    }

    public bool SetEquals(TwoValues v)
    {
        return X == v.X ? Y == v.Y
            : X == v.Y && Y == v.X;
    }
}

public class OrderedTwoValues : TwoValues
{
    // (架空の機能) 引数に対する高度な制約。
    public OrderedTwoValues(int x, int y)
        : base(x, y) where x <= y
    {
    }
}


 

int[] や List<int> の代わりに、TwoValues クラスを定義して 2 つの整数を表現しています。
また、TwoValues クラスを継承して、順序を保持する OrderedTwoValues クラスを定義します。
このコンストラクターにある「where x <= y」は、
静的チェックのレベルで引数が x <= y を満たした状態でコンストラクターを呼び出さなければ、
コンパイルがエラーとなることを意味することにします。

そして、並べ替えを表す Sort メソッドの引数を TwoValues 型、戻り値を OrderedTwoValues 型とします。
これにより、条件 1 が保証されます。

さらに、Sort メソッドに対する制約として「where Sort(v).SetEquals(v)」を追加します。
SetEquals メソッドは ISet<T>.SetEquals メソッドと同様、集合として等しいかどうかを判定します。
これにより、条件 2 が保証されます。

このように強力な制約を導入することで、メソッドのシグネチャだけで条件 1, 2 を表現できました。
ということは、コンパイルが成功するように実装するだけで、このメソッドにはバグが存在しないことが保証されます。
(上記の時点の実装では NotImplementedException が発生するため、条件 2 を満たさず、コンパイルはエラーとなります。)

では、いよいよ Sort メソッドの実装です。


static OrderedTwoValues Sort(TwoValues v) where Sort(v).SetEquals(v)
{
    // コンパイルが成功するための実装。
    return v.X <= v.Y
        ? new OrderedTwoValues(v.X, v.Y)
        : new OrderedTwoValues(v.Y, v.X);
}

 

new OrderedTwoValues(v.X, v.Y) の部分は v.X <= v.Y を満たすスコープの中にいるため、
OrderedTwoValues コンストラクターの制約 x <= y を満たすはずです。
また、new OrderedTwoValues(v.Y, v.X) の部分は v.Y < v.X を満たすスコープの中にいるため、この制約を満たすはずです。

人間が数学の証明をするとき、具体的な数値を代入しなくても、変数のまま大小関係を判定します。
もしコンパイラがもう少し賢くなれば、この程度の判断は十分可能でしょう。

同様に、OrderedTwoValues コンストラクターの引数には、一方に v.X を、他方に v.Y を渡しているため、
Sort(v).SetEquals(v) を満たします。
ここで例えば return new OrderedTwoValues(0, 1) などと実装してしまうと、コンパイル エラーとなります。

というわけで、上記の実装によりコンパイルは成功し、同時に正しい実装であることが保証されます。
このような手法は形式的検証 (formal verification) と呼ばれ、バグが存在してはならないソフトウェアを作成するときなどに利用されます。
C# においても、そのうち Roslyn をベースとして形式的検証のできるコンパイラが登場するのではないでしょうか。

 

作成したサンプル
SortConsole (GitHub)
MathConsole (GitHub)

参照
形式的検証 – Wikipedia
プログラミング Coq
証明駆動開発入門

広告

LINQ で素数を求める (C#)

素数を求める .NET (C#) のプログラムを、LINQ to Objects を利用して作成します。

素数を「自分自身より小さいすべての素数で割り切れない数」と解釈すれば、次のように実装できます。
引数に求める素数の範囲の最小値と最大値を指定できる関数として作成しています。

Program.cs


using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;

namespace PrimeNumbersConsole
{
    class Program
    {
        static void Main(string[] args)
        {
            var stopwatch = Stopwatch.StartNew();
            var result = GetPrimeNumbers_Alpha(1000, 1100).ToArray();
            stopwatch.Stop();

            Array.ForEach(result, Console.WriteLine);
            Console.WriteLine("{0} seconds", stopwatch.Elapsed.TotalSeconds);
        }

        static readonly Func<long, long, IEnumerable<long>> GetPrimeNumbers_Alpha = (minValue, maxValue) =>
            new[] { new List<long>() }
                .SelectMany(primes => Enumerable2.Range2(2, maxValue)
                    .Select(i => new { primes, i }))
                .Where(_ => _.primes
                    .All(p => _.i % p != 0))
                .Do(_ => _.primes.Add(_.i))
                .Select(_ => _.i)
                .SkipWhile(i => i < minValue);
    }

    public static class Enumerable2
    {
        public static IEnumerable<long> Range2(long minValue, long maxValue)
        {
            for (var i = minValue; i <= maxValue; i++)
            {
                yield return i;
            }
        }

        public static IEnumerable<TSource> Do<TSource>(this IEnumerable<TSource> source, Action<TSource> action)
        {
            if (source == null) throw new ArgumentNullException("source");
            if (action == null) throw new ArgumentNullException("action");

            foreach (var item in source)
            {
                action(item);
                yield return item;
            }
        }
    }
}


素数を小さい順にキャッシュしておくための List<long> オブジェクトを最初に用意し、
それを各イテレーションで参照できるようにしています。
また、実装を概念的にシンプルにするため、拡張メソッドを自作しています (Range2, Do メソッド)。

 

さて、これを少し工夫すると、実行速度を大きく改善できます。

  • ある数が割り切れるとき、その約数の対は、一方が平方根以下の約数、他方が平方根以上の約数となるので、
    平方根以下の素数で割り切れるかどうかだけを調べれば十分である。
  • これに伴い、maxValue の平方根以下の素数だけをキャッシュさせておけば十分である。

これらの考慮を反映させると次のようになります。


static void Main(string[] args)
{
    var stopwatch = Stopwatch.StartNew();
    var result = GetPrimeNumbers(1000000000000, 1000000001000).ToArray();
    stopwatch.Stop();

    Array.ForEach(result, Console.WriteLine);
    Console.WriteLine("{0} seconds", stopwatch.Elapsed.TotalSeconds);
}

static readonly Func<long, long, IEnumerable<long>> GetPrimeNumbers = (minValue, maxValue) =>
    new[]
    {
        new
        {
            primes = new List<long>(),
            min = Math.Max(minValue, 2),
            max = Math.Max(maxValue, 0),
            root_max = maxValue >= 0 ? (long)Math.Sqrt(maxValue) : 0,
        }
    }
        .SelectMany(_ => Enumerable2.Range2(2, Math.Min(_.root_max, _.min  1))
            .Concat(Enumerable2.Range2(_.min, _.max))
            .Select(i => new { _.primes, i, root_i = (long)Math.Sqrt(i) }))
        .Where(_ => _.primes
            .TakeWhile(p => p <= _.root_i)
            .All(p => _.i % p != 0))
        .Do(_ => _.primes.Add(_.i))
        .Select(_ => _.i)
        .SkipWhile(i => i < minValue);


 

この実装であれば、1 兆前後の素数でも、最近のタブレット PC で 1 秒以内で求められます。

実行結果

 

ちなみに、素数の定義通りに実装するのであれば、次のようなシンプルな実装で済みます。


static readonly Func<long, long, IEnumerable<long>> GetPrimeNumbers_Org = (minValue, maxValue) =>
    Enumerable2.Range2(Math.Max(minValue, 2), maxValue).Where(i =>
        Enumerable2.Range2(2, i  1).All(j => i % j != 0));


 

F# 版も書きました: F# で素数を求める

 

作成したサンプル
PrimeNumbersConsole (GitHub)

バージョン情報
.NET Framework 4.5

参照
エラトステネスの篩 – Wikipedia
F# で素数を求める

カテゴリー: .NET Framework. タグ: . 2 Comments »

Kinect で背景を除去するツール

Kinect for Windows (v1) を使用して、
カメラの画像から人物の部分を切り抜いて (背景を取り除いて) 表示するためのデスクトップ アプリ Portrait Clip を作成しました。
セットアップ方法、使用方法も Portrait Clip のページに記載してあります。

画像をマウスやタッチで直接ドラッグすれば移動させることができます。
また、画像を右クリックしてウィンドウの枠を表示させ、その枠をドラッグすれば画像を拡大・縮小できます。

オンライン セミナーなど、資料を全画面で表示しつつ人物も同時に表示したい場合に活用できると思います。

Portrait Clip

 

バージョン情報
.NET Framework 4.5
Kinect for Windows Runtime v1.8

参照
Portrait Clip (GitHub)

Excel ファイルから画像を自動で取り出す

Excel シートに貼り付けられた画像をファイルとして取得する、というのを .NET (C#) のプログラムで実現する方法を示します。

拡張子が .xlsx (Open XML 形式) の Excel ファイルの実体は ZIP ファイルとなっており、
中には XML ファイルや画像ファイルが格納されています。
画像ファイルは、 xl/media フォルダーに存在します。

xl/media フォルダー

 

これを .NET Framework 4.5 で追加された ZipFile クラスを利用して取り出すことを考えます。

単に ZIP ファイルからすべてのファイルを展開するだけであれば ZipFile.ExtractToDirectory メソッドを、
逆に、フォルダーにあるすべてのファイルを圧縮するだけであれば ZipFile.CreateFromDirectory メソッドを呼び出します。
それぞれ 1 行だけコードを書けば終了です。

ですが、今回は ZIP ファイルの中から一部のファイルだけを取り出すため、ZipFile.OpenRead メソッドを利用します。
参照に System.IO.Compression.dll と System.IO.Compression.FileSystem.dll を追加して、
Program.cs を次のように実装します。


using System;
using System.Collections.Generic;
using System.IO;
using System.IO.Compression;
using System.Linq;

namespace ExcelMediaConsole
{
    class Program
    {
        static void Main(string[] args)
        {
            var excelFilePath = "Book1.xlsx";
            var outputDirPath = "Media";

            Directory.CreateDirectory(outputDirPath);

            using (var archive = ZipFile.OpenRead(excelFilePath))
            {
                var query = archive.Entries
                    .Where(e => e.FullName.StartsWith("xl/media/", StringComparison.InvariantCultureIgnoreCase));

                foreach (var entry in query)
                {
                    var filePath = Path.Combine(outputDirPath, entry.Name);
                    entry.ExtractToFile(filePath, true);
                }
            }
        }
    }
}


 

xl/media フォルダーに存在するファイルを抽出して展開します。
通常の ZIP ファイルのパスの区切り文字は \ ですが、Excel ファイルの場合は / となっており、注意が必要です。

このプログラムを実行すれば、Media フォルダーに画像ファイルが保存されます。

取得した画像ファイル

この仕組みを使ってバッチ処理化もできるでしょう。
なお、Word や PowerPoint のファイルに対しても、同様の方法で画像ファイルを取り出せるようです。

 

作成したサンプル
ExcelMediaConsole (GitHub)

バージョン情報
.NET Framework 4.5

参照
ZipFile クラス
PowerShellでOpen XML形式のMS Officeに保存された画像ファイルを抽出する
Excel 方眼紙でドット絵を描く
Open XML SDK で Excel シートを読み込む

カテゴリー: .NET Framework. タグ: , , . 1 Comment »