Alloyハンズオン企画

126 views
Skip to first unread message

Takeo Imai

unread,
Mar 25, 2012, 7:37:43 PM3/25/12
to allo...@googlegroups.com
今井です。

GWあたりに都内でAlloyのハンズオンのようなものをやったら、皆さん参加します?
もしやるとしたらこういう話が聞きたい、などのご要望もあれば、お願いします。

--
IMAI Takeo <takeo...@gmail.com>

taichi sato

unread,
Mar 26, 2012, 12:52:57 AM3/26/12
to allo...@googlegroups.com
初めまして、佐藤太一です。

是非参加したいです。
事前にハンズオン課題を出して頂けると嬉しいです。

Takeo Imai

unread,
Mar 28, 2012, 6:32:50 PM3/28/12
to allo...@googlegroups.com
今井です。

佐藤さん、ありがとうございます。
あ、課題は事前に出したほうがいいですか。うーむ。
こういうのはぶっつけ本番的にやるのがいいかとも思っていたのでw せいぜい
「Alloy Analyzer をインストールしといてください」、というくらいのつもりでした。
どうしようかなぁ。

あと日程ですが、よく考えるとGW前半は予定が入っていたので、
GW後半か、翌週の週末あたりになるかもです。

ATNDにとりあえずイベント上げてみますかね…


On Mon, Mar 26, 2012 at 1:52 PM, taichi sato <ryu...@gmail.com> wrote:
> 初めまして、佐藤太一です。
>
> 是非参加したいです。
> 事前にハンズオン課題を出して頂けると嬉しいです。

--
IMAI Takeo <takeo...@gmail.com>

Takeo Imai

unread,
Mar 28, 2012, 6:52:18 PM3/28/12
to allo...@googlegroups.com
と、いうことで、ATNDにイベントを上げてみました。
http://atnd.org/events/27160

日程も会場もこれからですが、希望の方は参加表明お願いします。

今井
--
IMAI Takeo <takeo...@gmail.com>

nagaku@nii

unread,
Mar 28, 2012, 10:08:08 PM3/28/12
to allo...@googlegroups.com
今井さま

お世話になります、長久です。

TDDをご存知であればイメージしてもらいやすいのですが、
TDDBCというイベントがあって、
そこでは、漸近的に満たすべき要求が与えられて、
それに合わせてテストを書き加えて、
実装を作り込んでいく、という反復開発をやります。
(ペアプロで)

Alloyの本も導入部では同じような流れだったかと思うのですが、
段階的に提供される要求チケットを、ペアモデリングでこなして、
モデルを作り込んでいく、AlloyBCとか面白そうだなと思いました。

coqもBC形式でもっと間口広がるかもなー。

宜しくお願い致します。
--
国立情報学研究所 特任技術専門員
早稲田大学MNC 非常勤講師
長久 勝(Masaru Nagaku)
TEL:03-4212-2830
FAX:03-4212-2697
http://kgr-lab.ddo.jp/

2012年3月29日7:32 Takeo Imai <takeo...@gmail.com>:

Takeo Imai

unread,
Mar 29, 2012, 9:51:21 AM3/29/12
to allo...@googlegroups.com
長久さん、どうもです。

ペアモデリングですか。面白そうですね。
実は自分も職場でたまにペアモデリングのようなことをすることがあり
(2人とは限らないのですが)
会議でアイデアを詰めたいときに、その場でAlloy Analyzerを起動してモニタに映し、
ちょこちょこと書いて動かして、出てきた結果を見ながら2, 3人で議論したり修正かけたり、
といったことをたまにしています。

当日そういう経験談をしようかなーとはぼんやり思っていたんですが、実際にやってみる
という発想はなかったです。

ただ、ちょっと具体的なイメージが沸いてないところがあるのですが

1. 要求は開催前に提示されるのでしょうか? その場で順次追加されていく感じなのでしょうか?

2. そういうイベントでは、ペアってどうやって決めてるのでしょう?(^^;

--
IMAI Takeo <takeo...@gmail.com>

Takashi MIYAMOTO

unread,
Mar 29, 2012, 10:28:11 AM3/29/12
to allo...@googlegroups.com, Takashi MIYAMOTO
tmiya_です

On 2012/03/29, at 11:08, nagaku@nii wrote:

> お世話になります、長久です。


>
> そこでは、漸近的に満たすべき要求が与えられて、
> それに合わせてテストを書き加えて、
> 実装を作り込んでいく、という反復開発をやります。
> (ペアプロで)
>

> coqもBC形式でもっと間口広がるかもなー。

Alloyの話ではなくCoqの話になるのでオフトピックですがご容赦を。

先日Coqチュートリアルした時に、pair-provingしてもらったのですが、
- 1人より2人の方が行き詰まりにくい
- 1画面でCoqを開き、別の画面で資料を読めるので便利
などの理由で、pair-provingは好評でした。それは実績があります。

一方で漸近的に要求が与えられるというのはうまくやらないと厳しいかも。
というのは、証明課題が増える分には構わないのだけれど、根元の定義が
変わると、いままでにやった証明全部やり直しになる可能性があるので。

#例えば、<式> ::= <数> | <項> + <式> だったのが
#<式> ::= <数> | <項> + <式> | <項> * <式> に突然増えたら、
#<式>に関する証明、全部やり直しですし。。。

まぁ反復開発に「最初からからもう一度やりなおし」が有っても良いし、
積んだ経験は無駄にはならないし、コピペ再利用も可能ですけどね。

===================================
Takashi Miyamoto


nagaku@nii

unread,
Mar 29, 2012, 12:00:11 PM3/29/12
to allo...@googlegroups.com
今井さま

お世話になります、長久です。

> 1. 要求は開催前に提示されるのでしょうか? その場で順次追加されていく感じなのでしょうか?

お題の例です。

http://devtesting.jp/tddbc/?TDDBC%E6%9D%B1%E4%BA%AC1.6%2F%E8%AA%B2%E9%A1%8C

現地でペアを組んだ後、最初の課題が提示され、
課題が出来たら(TDDBCの場合、課題をテストに表現して、それを通せる実装が出来たら)
次の課題を書いたチケットを貰いに行く、という感じです。
事前提示ではなく、ペアの進捗に合わせて課題をもらっていきます。
公文式みたいな感じ?

課題は、前の課題に要求を追加していくようになっていて、
徐々に実装の機能が増えていくようになっています。
課題間のギャップが大きすぎると、作業をこなすテンポが悪くなるので、
課題設定は結構難しいなと思います。

> 2. そういうイベントでは、ペアってどうやって決めてるのでしょう?(^^;

私が関わった回では、現地で関連スキルをざっくり聞いて順序付けし、
1-10までいたら、1と6、2と7、3と8、4と9、5と10、で組みました。
ペアの2人にスキル差がありすぎると、1人が教えてもらうだけになってしまうし、
ペアの集合におけるスキルの分散が大きいと、課題が簡単すぎたり難しすぎたりするので、
この決め方を採用していたようです。

宜しくお願い致します。
--
国立情報学研究所 特任技術専門員
早稲田大学MNC 非常勤講師
長久 勝(Masaru Nagaku)
TEL:03-4212-2830
FAX:03-4212-2697
http://kgr-lab.ddo.jp/

2012年3月29日22:51 Takeo Imai <takeo...@gmail.com>:

nagaku@nii

unread,
Mar 29, 2012, 12:02:03 PM3/29/12
to allo...@googlegroups.com
あ、Alloyでやる場合は、お題の構成として、
段階的詳細化を意識させる流れで上手く行くと思います。


2012年3月30日1:00 nagaku@nii <nag...@nii.ac.jp>:

西尾泰和

unread,
Apr 5, 2012, 12:42:20 AM4/5/12
to Alloy-jp
はじめまして、西尾泰和(@nishio)です。
ハンズオン楽しみにしています!

ペアモデリングは楽しそうですね。
お題に関して、個人的にはいま教科書の6章の事例を眺めていて
時系列で変化する状態のモデリングがいまいちピンと来ないので
「-> Time」の導入のあたりを噛み砕いて教えてもらえるとうれしいです。

以前檜山さんが人生をAlloyでモデリングされてましたが、
あれの続きを自分でやろうとして
「結婚をするとPersonの状態がNotMarriedからMarriedに変わる」
みたいなことをどう記述するのがスマートかわからず混乱しています。

Masayuki Hiyama

unread,
Apr 5, 2012, 12:56:10 AM4/5/12
to allo...@googlegroups.com
> 以前檜山さんが人生をAlloyでモデリングされてましたが、

もうやる気がなくなったので、続きはお任せします。よろしくお願いします。


--
檜山正幸 (HIYAMA Masayuki)

http://d.hatena.ne.jp/m-hiyama/
http://www.chimaira.org/

Takeo Imai

unread,
May 12, 2012, 1:10:05 AM5/12/12
to allo...@googlegroups.com
皆様

明日、開催です。参加予定の方はお忘れなきよう。
http://atnd.org/events/27160

--
IMAI Takeo <takeo...@gmail.com>

Takeo Imai

unread,
May 13, 2012, 7:57:22 AM5/13/12
to allo...@googlegroups.com
皆様

今日はお疲れ様でした。
ATNDのイベント告知サイトに、資料へのリンクなどを追加しておきました。
http://atnd.org/events/27160

本日を受けて、ご感想・ご意見・次回に向けてのご要望などあれば、このMLでも、私個人宛でも結構ですので、教えていただけると助かります。
個人的には、折を見て第2回も企画してみようかなと思っています。

最後に、今回 企画・運営に小林さん、小笠原さんに多大なご協力いただきました。
この場を借りて感謝します。

--
IMAI Takeo <takeo...@gmail.com>

Takeo Imai

unread,
May 14, 2012, 9:48:17 AM5/14/12
to allo...@googlegroups.com
皆様
今井です。

当日、頂いた質問の1つにうまく答えられなかったのですが、改めて回答を自分のブログに書きました。ご参考まで。
http://d.hatena.ne.jp/bonotake/20120514/1337002401

# 細かくてややこしい話なので、興味ない方は無視して頂いて結構です。


2012/5/13 Takeo Imai <takeo...@gmail.com>:
--
IMAI Takeo <takeo...@gmail.com>
Reply all
Reply to author
Forward
0 new messages