未分類部分文字列を取得する関数で悩みたくない！
部分文字列を取得する関数で悩みたくない！ 文字列から部分文字列を抜き出す組み込み関数がよくうろ覚えになっていたのですが，うろ覚えにならずに済む考え方に至ったのでそのメモです． 部分文字列 与えられた 0 文字以上の文字列から，一部または全部...
未分類AlloyAlloy で形式手法を始めてみた！～述語，関数，実行編～
Alloy で形式手法を始めてみた！～述語，関数，実行編～ ここでは，述語 (pred) や関数 (fun) の書き方を説明します．その前に，述語内に記述する 条件式について説明します． 条件式 述語を説明する前に，プログラミングでいう i...
AlloyAlloy で形式手法を始めてみた！～集合の演算・発展編～
Alloy で形式手法を始めてみた！～集合の演算・発展編～ ここでは，集合に対する発展的な演算を説明します． 集合と関係式の演算 集合と関係式の演算には，ドットジョインがあります． ドットジョイン Alloy では，集合と関係式，あるいは関...
AlloyAlloy で形式手法を始めてみた！～集合の演算と数値編～
Alloy で形式手法を始めてみた！～集合の演算と数値編～ ここでは，集合に対する演算と数値の扱いについて説明します． 集合の演算 集合の演算には， +, -, &, -> の四つがあります． + + は和集合を表します．...
AlloyAlloy で形式手法を始めてみた！～特殊なシグネチャ編～
Alloy で形式手法を始めてみた！～特殊なシグネチャ編～ ここでは，シグネチャ編で話さなかった，以下の内容を話します． "継承" したときに，継承元のフィールドはどうなるか？ Enum とはなにか？ 特殊な集合 i...
AlloyAlloy で形式手法を始めてみた！～関係式の多重度編～
Alloy で形式手法を始めてみた！～関係式の多重度編～ 関係式とは？ シグネチャ同士のつながり関係を表す条件式を関係式といいます． これもある種のフィールドとして扱います． フィールドについてはこちらで説明しています． 多項関係 シグネチ...
AlloyAlloy で形式手法を始めてみた！～シグネチャ編～
Alloy で形式手法を始めてみた！～シグネチャ編～ Signature とは？ Signature（シグネチャ）はオブジェクト指向プログラミングでいうオブジェクトに相当します．人や状態，DB のレコード，ファイルなど，モノを表すための基本...
AlloyAlloy で形式手法を始めてみた！～導入編～
Alloy で形式手法を始めてみた！～導入編～ Alloy とは Alloy は構造の記述とその探索のためのツール．例えば，セキュリティホールの発見や，定義されたネットワークトポロジーの中で起こりうる構造の列挙するなど，定義を書いてその例を...
Alloy【形式手法】ボウリング第 10 フレームを Alloy と TLA+ (PlusCal) で定式化
ボウリングの第 10 フレームの定式化を Alloy と TLA+ (PlusCal) でやってみる Alloy と TLA+ (PlusCal) の使い方が徐々にわかってきたので，実際に仕様を書いてみます． ボウリングの第 10 フレーム...
YouTubeStrange Loop の動画で形式手法の事例をみる
自宅で熟成させている TLA+ の書籍の著者名でググったり YouTube の動画を探したりしているといくつか出てきました． その中で，Alloy も含めて形式手法の事例の紹介の動画が見つかったので，その動画の大本になっている "...