Alloyを使って有限群を調べてみる - ashiato45の日記
Alloyはモノを抽象的に記述したり、それらの関係を数学で言うところの「関係」でもって記述する言語です。 さらに、そこで記された制約を満足する例を見つけたり、制約に対する反例を見つけたりするための解析器がついてます。 プログラムの仕様をこれで記述して、それに対して見落しがないかを探すのに便利みたいです。 公式サイトhttp://alloy.mit.edu/alloy/の記述を引用すると、 Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching net
Alloy Analyzer で形式仕様記述
仕様を形式的に記述/検査することのできる言語やツールは、VDM, B, Z, Isabelle など他にも色々ありますが、 Alloy はそれらにくらべてより軽いフットワークで記述/検査することができるツールです。 それらのツールと Alloy との比較も、機会があればご紹介したいと思います。 2. Alloy を使った形式仕様記述の特徴 数理論理学＋集合論をベースとした Alloy の言語で仕様を記述します。 書いた仕様を、簡単に検査することができます。 難しい論理式の証明などは必要ありません。 検査結果は図で表示してくれるので、結果を目視で直感的に理解することができます。 仕様で書いた振る舞いをシミュレーションすることができます。 3. このページのスコープ ここでは仕様のうち、概要レベルの仕様や、重要な部分だけを抜き出した仕様といった、抽象度の高い仕様をスコープとしています。 抽象度
Alloy でクリプキ可能世界意味論！ - これは圏です（はてな使ったら負けだとおもっていた）
Alloy でクリプキの可能世界意味論をエンコードしてみた記録。 論理学をきちんと勉強した訳じゃないので、もし誤りがあったら是非教えてください。 可能世界意味論と云うのは、偉大な論理学者ソール・クリプキが、なんと高校生の頃に思い付いた様相論理の意味論です。 様相論理って云うのは、通常の命題論理に、「□P (必然的に P)」とか「◇P (Pであることが可能)」と云う二つの記号を付け加えて出来る論理体系です。要は可能性を扱う論理学ですね！ ひとくちに様相論理と云っても色々種類があるそうで、「必然的にP なんだったらどう考えてもPだろうよ」「必然的にPであるためにはまずPが可能じゃないといけないんじゃね？」「必然から可能が必然だよな*1！」とかみんな色々な法則を提唱してるんだとか。みんながみんなオレオレ様相論理を作るので、それぞれが一体どういう関係にあるのか？とか、本当にそれで大丈夫なの？とか、
形式手法とモデリング - AlloyAnalyzerを中心に
2.3. モデリング・セッション1: 最小限の仕様を作る 今回、実際にモデリングする対象は、以下に示す、簡単なロール・ベース・アクセス制御（Role-Based Access Control: RBAC）の仕様です。 集合 ユーザー（User）: ユーザー・アカウント ロール（Role）: ユーザーに割り当てられる役割。Administrator、Guestなど 権限（Permission）: 役割に割り当てられる権限。Read、Write、Read Writeなど ユーザーは、0以上のロールを持つ ロールは、0以上の権限を持つ Alloy Analyzerでは、最初から一気に仕様を書き上げることは、あまり行ないません。まずは最小限の仕様を作成したうえで、検証を繰り返しながら仕様を追加していきます。 2.3.1. 集合の記述 最初はまず、最低限の仕様を作りましょう。 これだけです。 いくつ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
書籍『抽象によるソフトウェア設計－Alloyではじめる形式手法－』の紹介
