Alloy

Alloy で形式手法を始めてみた！～述語，関数，実行編～ ここでは，述語 (pred) や関数 (fun) の書き方を説明します．その前に，述語内に記述する 条件式について説明します． 条件式 述語を説明する前に，プログラミングでいう i...

Alloy で形式手法を始めてみた！～集合の演算・発展編～ ここでは，集合に対する発展的な演算を説明します． 集合と関係式の演算 集合と関係式の演算には，ドットジョインがあります． ドットジョイン Alloy では，集合と関係式，あるいは関...

Alloy で形式手法を始めてみた！～集合の演算と数値編～ ここでは，集合に対する演算と数値の扱いについて説明します． 集合の演算 集合の演算には， +, -, &, -> の四つがあります． + + は和集合を表します．...

Alloy で形式手法を始めてみた！～特殊なシグネチャ編～ ここでは，シグネチャ編で話さなかった，以下の内容を話します． "継承" したときに，継承元のフィールドはどうなるか？ Enum とはなにか？ 特殊な集合 i...

Alloy で形式手法を始めてみた！～関係式の多重度編～ 関係式とは？ シグネチャ同士のつながり関係を表す条件式を関係式といいます． これもある種のフィールドとして扱います． フィールドについてはこちらで説明しています． 多項関係 シグネチ...

Alloy で形式手法を始めてみた！～シグネチャ編～ Signature とは？ Signature（シグネチャ）はオブジェクト指向プログラミングでいうオブジェクトに相当します．人や状態，DB のレコード，ファイルなど，モノを表すための基本...

Alloy で形式手法を始めてみた！～導入編～ Alloy とは Alloy は構造の記述とその探索のためのツール．例えば，セキュリティホールの発見や，定義されたネットワークトポロジーの中で起こりうる構造の列挙するなど，定義を書いてその例を...

Alloy Analyzer について軽く文法を調べれたので，試しに動かしてみました． サンプル 問題 A, B, C, D の 4 人は，総務，外務，財務，防衛の 4 つの大臣に重複なく割り振られる．割り振りに関して，以下の情報が得られた...

永遠の暫定版．間違ってたらコメント下さい．わからないで書いているところもあるので，ほぼ私のためのメモになっています…（言い訳）． 全体像 モジュールヘッダ module hoge から書く．書いているモデルのモジュール名に当たると思われる...