prepress-tips

形式手法モデル理論アプローチ

最終更新：2008年10月28日 12:50

prepress-tips

- view

管理者のみ編集可

　狼・山羊・キャベツの川渡し問題を perlや javascriptを使って形式手法モデル理論アプローチで解く。

最終更新日時： 2008/10/28

形式手法とその利点

狼・山羊・キャベツの川渡し問題とは

perlで狼・山羊・キャベツの川渡し

javascriptで狼・山羊・キャベツの川渡し

perlscriptを javascriptに書き換える要領

Edit

形式手法とその利点

オブジェクト指向は、モジュールを外部から見たときの挙動に関してとても詳しい情報を与えてくれるが、その内部構造に関しては何の情報も与えてくれない。
UMLによるモデリングも同様で、いざコードを作ろうとすると ─ はて？─ と戸惑うことになる。
形式手法は、モジュール内部の構造がどう記述されなくてはならないという指針を明快に与えてくれるので、構造はわかりやすく機械的にコードを作ることすら可能である。
if や for をあまり使う必要がなくこの面で悩まされることが少ない。
大規模なプログラムに適用されることが多いようであるが、perlや javascriptで書くテストも作らないような小規模のプログラムにも十分有効である。
プログラムの異なる言語間の移植にもとても有用に思われる。
形式手法の教科書は『形式手法モデル理論アプローチ』高原他著日科技連刊
- 集合やオートマトンなどの用語が並んでいるが、プログラミング経験豊富なら
  3章の始めの1節と 5章の始めの2節に目を通せばおおよその把握はできる。
- 先にこのページの wgc2.pl ソースを見るのもよいかも。
- この頁よりもっと実際的なサンプルを作成中。
  → 形式手法モデル理論アプローチ２　形式手法モデル理論アプローチ３
- この方法の応用を検討中。 → 対話・検索・選択によるプログラミング

狼・山羊・キャベツの川渡し問題とは

狼・山羊・キャベツの川渡し問題とは、古典的なパズルのようで次のような問題。

  農夫が狼・山羊・キャベツと一緒に川の左岸におり、
  これらを川の右岸へ運ばなくてはいけないのだが、
  ボートにはこれらのうち１つしか乗せることができず、
  狼は山羊を好んで食べるので 狼・山羊を同じ岸に放置できず、
  山羊はキャベツを好んで食べるので 山羊・キャベツも同じ岸に放置できない。
  ただし ボートに農夫だけが乗ることは許される。
  この条件で すべてを右岸へ運ぶ手順を求めるという問題。

perlで狼・山羊・キャベツの川渡し

まずは教科書通りに作成。
実行は perl wgc.pl 。
テスト用の汎用バッチファイル（ test.bat ）を wgc.bat にリネームして実行してもよい。

wgc.pl

#- このプログラムは ？
#    狼・山羊・キャベツの川渡し問題を perlを使って 形式手法モデル理論アプローチで 解く

#- まず 問題を記述する。
#    川の左側を State とする。Setは 集合。

sub All { Set( "f", "w", "g", "c" ); } # 全体集合

sub InitialState { All; } # 初期 State
sub FinalState { Set(); } # 求める State

sub Actions { # どんなアクションが可能か？
    my $left = $_[0]; my $right = All->Minus( $left );
    my $attention = $left->contain( "f" ) ? $left : $right ;
    ( map do { Set( $_ ); }, $attention->Members );
}
sub Delta { # アクションを実行したあとの Stateは？
    my $left = $_[0]; my $action = Set( "f" )->Add( $_[1] );
    $left->contain( "f" ) ? $left->Minus( $action ) : $left->Add( $action ) ;
}
sub constraint { # 守らなくてはいけないこと
    my $left = $_[0]; my $right = All->Minus( $left );
    my $attention = $left->contain( "f" ) ? $right : $left ;
    ! $attention->contain( "w", "g" ) && ! $attention->contain( "g", "c" );
}
sub goal { $_[0]->equal( FinalState ); } # ゴール

sub asString { join ' ', $_[0]->Members; } # goal-seeker のための補助メソッド

#-- 以下は Set（ 集合 ）の操作。

sub Set {
    my %h = map do { ( $_, 1 ); }, @_;
    my $s = bless {}; $s->{ members } = [ sort { $a cmp $b } keys %h ];
    return $s;
}
sub Members { @{ $_[0]->{ members } }; }

sub contain {
    my %h = map do { ( $_, 1 ); }, ( shift @_ )->Members;
    for( @_ ) { defined( $h{ $_ } ) || return 0; }
    return 1;
}
sub Minus {
    Set( map do { $_[1]->contain( $_ ) ? () : $_ ; }, $_[0]->Members );
}
sub Add {
    Set( $_[0]->Members, $_[1]->Minus( $_[0] )->Members );
}
sub equal {
    my @s0 = $_[0]->Members; my @s1 = $_[1]->Members;
    while( @s0 && @s1 ) { shift @s0 eq shift @s1 || return 0; }
    return ! @s0 && ! @s1;
}

#- 問題を goal-seekerで 解く。
#    goal-seekerは 多くの問題に共通に利用できる。

{
    msg( '狼・山羊・キャベツの川渡し問題：' );
    GoalSeeker( 0 )->goal_seek( InitialState );
    msg( '  finished.' ); `pause`;
    exit( 0 );
}
sub msg { map do { print "$_\x0a"; }, @_; }

sub GoalSeeker {
    my $gs = bless {}; {
        $gs->{ debug } = $_[0];
        $gs->{ ActionSequence } = [];
        $gs->{ StateHistory } = {};
    }
    $gs->{ debug } && msg( '  debug mode' );
    return $gs;
}
sub debug { $_[0]->{ debug }; }
sub ActionSequence { $_[0]->{ ActionSequence }; }
sub StateHistory { $_[0]->{ StateHistory }; }

sub goal_seek {
    my $state = $_[1]->asString;
    $_[0]->debug && ( msg( "  c: $state" ), `pause` );
    $_[1]->goal && ( msg( "  ".join ' → ', @{$_[0]->ActionSequence} ), `pause`, return );
    $_[1]->constraint || return;
    $_[0]->StateHistory->{ $state } && return; $_[0]->StateHistory->{ $state } = 1;
    for( $_[1]->Actions ) {
        $_[0]->debug && msg( "  a: ".$_->asString );
        push @{$_[0]->ActionSequence}, $_->asString;
        $_[0]->goal_seek( $_[1]->Delta( $_ ) );
        pop @{$_[0]->ActionSequence};
        $_[0]->debug && msg( "  -: $state" );
    }
    $_[0]->StateHistory->{ $state } = undef;
}

test.bat

Set（集合）の操作と goal_seeker は多くの問題に共通に使えるので
─ 問題を記述するだけで解法プログラムができあがる ─ ということになる。
そして perlなら、集合もオブジェクトも使わずに記述できるはず。

wgc2.pl

#- このプログラムは ？
#    狼・山羊・キャベツの川渡し問題を perlを使って 形式手法モデル理論アプローチで 解く

#- まず 問題を記述する。
#    川の左側を State とする。

sub All { "fwgc"; } # 全体

sub InitialState { unique( All ); } # 初期 State
sub FinalState { unique( "" ); } # 求める State

sub Actions { # どんなアクションが可能か？
    my $left = $_[0]; my $right = minus( All, $left );
    split "", unique( $left =~ /f/ ? $left : $right );
}
sub Delta { # アクションを実行したあとの Stateは？
    my $left = $_[0]; my $action = "f$_[1]";
    unique( $left =~ /f/ ? minus( $left, $action ) : $left.$action );
}
sub constraint { # 守らなくてはいけないこと
    my $left = $_[0]; my $right = minus( All, $left );
    my $attention = ( $left =~ /f/ ? $right : $left );
    @{[ $attention =~ /[wg]/g ]} < 2 && @{[ $attention =~ /[gc]/g ]} < 2;
}

sub goal { $_[0] eq FinalState; } # ゴール

#    補助のルーチン
sub unique { my $r = ""; for( sort split "", $_[0] ) { $r =~ s/($_|$)/$_/; } $r; }
sub minus { $_[0] =~ s/[$_[1]]//g; $_[0]; }

#- 問題を goal-seekerで 解く。
#    goal-seekerは 多くの問題に共通に利用できる。

{
    my $debug = 0;
    msg( '狼・山羊・キャベツの川渡し問題：', $debug ? '  debug mode' : () );
    goal_seeker( InitialState, [ $debug ] );
    msg( '  finished.' ); `pause`;
    exit( 0 );
}
sub msg { map do { print "$_\x0a"; }, @_; }

sub goal_seeker {
    my ( $state, $env, ) = @_; 1 < @{$env} || push @{$env}, ( [], {} );
    my ( $debug, $ActionSequence, $StateHistory, ) = @{$env};

    $debug && ( msg( "  c: $state" ), `pause` );
    goal( $state ) && ( goal_msg( $ActionSequence ), `pause`, return );
    constraint( $state ) || return;
    $StateHistory->{ $state } && return; $StateHistory->{ $state } = 1;
    for( Actions( $state ) ) {
        $debug && msg( "  a: $_" );
        push @{$ActionSequence}, $_;
        goal_seeker( Delta( $state, $_ ), $env );
        pop @{$ActionSequence};
        $debug && msg( "  -: $state" );
    }
    $StateHistory->{ $state } = undef;
}
sub goal_msg { msg( "  ".join ' → ', @{$_[0]} ); }

ブラウザから perlscriptで動かす。
※ html中の＜と＆はすべて半角に置換すること。
※ perlscriptはコマンドラインからも動く（実行は perl wgc_pls.pl ）。

wgc.html

wgc_pls.pl

#- このプログラムは ？
#    狼・山羊・キャベツの川渡し問題を perlを使って 形式手法モデル理論アプローチで 解く
#    ブラウザと コマンドラインの 両方から動く。

#- まず 問題を記述する。
#    川の左側を State とする。

sub All { "fwgc"; } # 全体

sub InitialState { unique( All ); } # 初期 State
sub FinalState { unique( "" ); } # 求める State

sub Actions { # どんなアクションが可能か？
    my $left = $_[0]; my $right = minus( All, $left );
    split "", unique( $left =~ /f/ ? $left : $right );
}
sub Delta { # アクションを実行したあとの Stateは？
    my $left = $_[0]; my $action = "f$_[1]";
    unique( $left =~ /f/ ? minus( $left, $action ) : $left.$action );
}
sub constraint { # 守らなくてはいけないこと
    my $left = $_[0]; my $right = minus( All, $left );
    my $attention = ( $left =~ /f/ ? $right : $left );
    @{[ $attention =~ /[wg]/g ]} < 2 && @{[ $attention =~ /[gc]/g ]} < 2;
}

sub goal { $_[0] eq FinalState; } # ゴール

#    補助のルーチン
sub unique { my $r = ""; for( sort split "", $_[0] ) { $r =~ s/($_|$)/$_/; } $r; }
sub minus { $_[0] =~ s/[$_[1]]//g; $_[0]; }

#- 問題を goal-seekerで 解く。
#    goal-seekerは 多くの問題に共通に利用できる。

sub run {
    my $debug = get_debug();
    msg_clr(); msg( '狼・山羊・キャベツの川渡し問題：', $debug ? '  debug mode' : () );
    goal_seeker( InitialState, [ $debug ] );
    msg( '  finished.' );
}
sub msg { map do { msg_add( "$_\x0a" ); }, @_; }

sub goal_seeker {
    my ( $state, $env, ) = @_; 1 < @{$env} || push @{$env}, ( [], {} );
    my ( $debug, $ActionSequence, $StateHistory, ) = @{$env};

    $debug && ( msg( "  c: $state" ) );
    goal( $state ) && ( goal_msg( $ActionSequence ), return );
    constraint( $state ) || return;
    $StateHistory->{ $state } && return; $StateHistory->{ $state } = 1;
    for( Actions( $state ) ) {
        $debug && msg( "  a: $_" );
        push @{$ActionSequence}, $_;
        goal_seeker( Delta( $state, $_ ), $env );
        pop @{$ActionSequence};
        $debug && msg( "  -: $state" );
    }
    $StateHistory->{ $state } = undef;
}
sub goal_msg { msg( "  ".join ' → ', @{$_[0]} ); }

#- 外部とのインタフェース

sub id { return $window->document->getElementById( $_[0] ); }
sub popup { $window->alert( join "\x0a", @_ ); }

sub get_debug {
    if( $window->{ in_browser } ) { id( "param" )->options->{ id( "param" )->selectedIndex }->value; }
    else { @ARGV && $ARGV[0]; }
}
sub msg_clr {
    if( $window->{ in_browser } ) { id( 'result' )->{ 'innerHTML' } = ""; }
}
sub msg_add {
    if( $window->{ in_browser } ) { $_[0] =~ s/\x0a/\x3cbr>$&/; id( 'result' )->{ 'innerHTML' } .= $_[0]; }
    else { print $_[0]; }
}

if( ! $window->{ in_browser } ) { run(); `pause`; }

1;

javascriptで狼・山羊・キャベツの川渡し

javascript に書き直してみた（ perlとほとんど同じように書けるので）。
※ html中の＜と＆はすべて半角に置換すること。

wgc_js.html

wgc.js

//- このプログラムは ？
//    狼・山羊・キャベツの川渡し問題を javascriptを使って 形式手法モデル理論アプローチで 解く

//- まず 問題を記述する。
//    川の左側を State とする。

function All () { return "fwgc"; } // 全体

function InitialState () { return unique( All() ); } // 初期 State
function FinalState () { return unique( "" ); } // 求める State

function Actions ( state ) { // どんなアクションが可能か？
    var left = state; var right = minus( All(), left );
    return unique( left.match( /f/ ) != null ? left : right ).split( "" );
}
function Delta ( state, action ) { // アクションを実行したあとの Stateは？
    var left = state; action = "f" + action;
    return unique( left.match( /f/ ) != null ? minus( left, action ) : left + action );
}
function constraint ( state ) { // 守らなくてはいけないこと
    var left = state; var right = minus( All(), left );
    var attention = ( left.match( /f/ ) != null ? right : left );
    var m1 = attention.match( /[wg]/g ); var m2 = attention.match( /[gc]/g );
    return ( m1 == null || m1.length < 2 ) && ( m2 == null || m2.length < 2 );
}

function goal ( state ) { return state == FinalState(); } // ゴール

//    補助のルーチン
function unique ( state ) {
    var r = ""; var s = state.split( "" ).sort();
    for( c in s ) { r = r.replace( new RegExp( "(" + s[ c ] + "|$)" ), s[ c ] ); }
    return r;
}
function minus ( state_a, state_b ) {
    return state_a.replace( new RegExp( "[" + state_b + "]", "g" ), "" );
}

//- 問題を goal-seekerで 解く。
//    goal-seekerは 多くの問題に共通に利用できる。

function run () {
    var debug = get_debug();
    msg_clr(); msg( '狼・山羊・キャベツの川渡し問題：', debug ? '  debug mode' : null );
    goal_seeker( InitialState(), new Array( debug ) );
    msg( '  finished.' );
}
function msg () {
    var array = msg.arguments;
    for( var m = 0; m < array.length; m++ ) { array[ m ] != null && msg_add( array[ m ] + "\x0a" ); }
}

function goal_seeker ( state, env ) {
    1 < env.length || env.push( new Array(), new Array() );
    var debug = env[ 0 ]; var ActionSequence = env[ 1 ]; var StateHistory = env[ 2 ];

    debug && msg( "  c: " + state );
    if( goal( state ) ) { goal_msg( ActionSequence ); return; };
    if( ! constraint( state ) ) { return; }
    if( StateHistory[ state ] ) { return; } else { StateHistory[ state ] = true; }
    var actions = Actions( state ); for( a in actions ) {
        debug && msg( "  a: " + actions[ a ] );
        ActionSequence.push( actions[ a ] );
        goal_seeker( Delta( state, actions[ a ] ), env );
        ActionSequence.pop();
        debug && msg( "  -: " + state );
    }
    delete StateHistory[ state ];
}
function goal_msg ( m ) { msg( "  " + m.join( ' → ' ) ); }

//- 外部とのインタフェース

function id ( i ) { return window.document.getElementById( i ); }
function popup ( array ) { window.alert( array.join( "\x0a" ) ); }

function get_debug () {
    return id( "param" ).options[ id( "param" ).selectedIndex ].value == 1;
}
function msg_clr () {
    id( 'result' ).innerHTML = "";
}
function msg_add ( m ) {
    id( 'result' ).innerHTML += m.replace( new RegExp( "\x0a", "g" ), function( m ){ return "\x3cbr>" + m; } );
}

//alert( "load: ok" );
/*
*/

実際にブラウザで試してみる → wgc_js.html （実行ボタンをクリックしてみてください）

perlscriptを javascriptに書き換える要領

perlscriptを javascriptに書き換えるのは結構面倒なのでその要領をまとめておく。

perlscriptを javascriptに書き換える要領

コメントの # を // に置き換える。
ローカル変数の my を var に置き換える。
関数の sub を function に置き換える。
関数の引数を定義するために { の前に () を挿入する。
関数の戻り値の前に return を挿入する。
関数の引数を書き換える（ $_[0], @_ など）。
- 不定長の引数の受け渡しには関数名.arguments を使う。
map は for を使った表現に書き変える。
for( @array ) { $_ } は for( i in array ) { array[ i ] } に書き変える。
文字列結合の . は + を使った表現に書き換える。
eq は == に書き換える。
メソッドの -> は . に書き変える。
- 連想配列の {} は [] に書き変える。
- オブジェクトのプロパティは . に書き変える。
関数はメソッドの表現に書き換える。
- 適用順が逆になるので注意。
関数の呼び出しには必ず () を付ける。
変数の $ を削除する。
- 文字列中にあるときは + を使った表現に書き換える。
配列の @ を削除する。
- スカラコンテキストは .length を使った表現に書き換える。
- push, pop, join などは .push() .pop() .join() に書き換える。
連想配列の % を削除する。
配列・連想配列の定義を new Array() を使った表現に書き換える。
- 暗黙の配列の定義に new Array() を追加する。
- perlの空配列 () は null を使った表現に書き換える。
連想配列への undef の代入を delete に書き換える。
正規表現を書き換える。
- match()
  - マッチしない場合 null が返る。
  - マッチした場合 gの指定がないとき最初にマッチした文字列が返る。
  - マッチした場合 gの指定があるとき配列が返る。
- replcae()
  - a =~ s/[$x]/y/g ならば a.replace( new RegExp( "[" + x + "]", "g" ), "y" )
  - a =~ s/(x)(y)/$&$1$2/g ならば
    a.replace( /(x)(y)/g, function( s, m1, m2 ){ return s + m1 + m2; } )
不要の () を削除する。
&& || のところを必要に応じ if() {} を使った表現に書き換える。
true false の変わりに 1 0 を使っているところなどを注意深く修正する。
書き換えが終わったら下記の構造を使って未確認ソースを少しずつ減らしていく。

確認済ソース
alert( "load: ok" );
/*
   未確認ソース
*/

Edit

「形式手法モデル理論アプローチ」をウィキ内検索

人気記事ランキング

最近更新されたページ

急上昇Wikiランキング

急上昇中のWikiランキングです。今注目を集めている話題をチェックしてみよう！

人気Wikiランキング

atwikiでよく見られているWikiのランキングです。新しい情報を発見してみよう！

新規Wikiランキング

最近作成されたWikiのアクセスランキングです。見るだけでなく加筆してみよう！

全体ページランキング

最近アクセスの多かったページランキングです。話題のページを見に行こう！

形式手法モデル理論アプローチ

形式手法とその利点

狼・山羊・キャベツの川渡し問題とは

perlで 狼・山羊・キャベツの川渡し

javascriptで 狼・山羊・キャベツの川渡し

perlscriptを javascriptに書き換える要領

更新履歴

perlで狼・山羊・キャベツの川渡し

javascriptで狼・山羊・キャベツの川渡し