※この商品はタブレットなど大きいディスプレイを備えた端末で読むことに適しています。また、文字だけを拡大することや、文字列のハイライト、検索、辞書の参照、引用などの機能が使用できません。 プリント・レプリカ形式のKindle本は、FireタブレットおよびKindle無料アプリ (Kindle for iOS、Kindle for Android、Kindle for PC、Kindle for Mac) でのみご利用可能です。Kindle E Ink端末およびKindle Cloud Readerではご利用いただけません。 ※この電子書籍は紙版書籍のページデザインで制作した固定レイアウトです。 Alloy（アロイ）を通じて形式手法を学ぶ 形式手法は、高度な信頼性が求められるソフトウェアの開発で利用されてきた、数学に基づく開発技術です。Alloy（アロイ）は、形式手法を誰もが実践できることを目指したツールであり、テストでは排除できないソフトウェアの欠陥について検証するためのものです。 本書は、""Software Abstractions: Logic, Language, and Analysis""の翻訳書です。Alloyによるさまざまな事例のモデリングを通じ、「アジャイルで軽量な形式手法」ともいえる技術を学びます。 監訳者序文 日本語版に寄せて 序文 謝辞 第1章　はじめに 第2章　ざっと一巡り 2.1 静的な側面：状態を調べる 2.2 動的な側面：操作を追加する 2.3 階層の導入 2.4 実行トレース 2.5 まとめ 第3章　論理系 3.1 3つの側面を持つ論理系 3.2 アトムと関係 3.3 スナップショット 3.4 演算子 3.5 制約 3.6 宣言制約と多重度制約 3.7 濃度制約と整数 第4章　言語 4.1 例題：自分が自身の祖父 4.2 シグネチャとフィールド 4.3 モデル図 4.4 型と型検査 4.5 ファクト、述語、関数、アサーション 4.6 コマンドとスコープ 4.7 モジュールと多相性 4.8 整数と算術演算 第5章　解析 5.1 スコープを網羅する解析 5.2 インスタンス、充足例、反例 5.3 非限定の全称限量子 5.4 スコープの選択と単調性 第6章　事例 6.1 リーダー選出問題 6.2 ホテルの客室施錠 6.3 メディア資産管理 6.4 メモリの抽象化 付録A　練習問題 A.1 論理の問題 A.2 単純なモデルを拡張する A.3 古典的パズル A.4 メタモデル A.5 小さなケーススタディ A.6 自由形式のケーススタディ 付録B　Alloy言語リファレンス B.1 字句 B.2 名前空間 B.3 文法. B.4 優先順位と結合性 B.5 意味論の基本 B.6 型とオーバーロード B.7 言語機能 B.8 関係式 B.9 整数式 B.10 ブール式 付録C　中核の意味論 C.1 Alloy の中核の意味論 付録D　図的記法 付録E　Alloy以外の手法 E.1 事例 E.2 B E.3 OCL E.4 VDM E.5 Z 付録F　Alloy Analyzerクイックガイド F.1 Alloy 解析器の起動 F.2 Alloy 解析器のGUI F.3 Alloy モデルの解析を行う F.4 Alloy 4の構文的機能 付録G　訳語一覧 参考文献 訳者あとがき 索引

クラウドが好きな大学生が読んで良さげだった本を紹介する

alloy analyzer入門

Alloyでパズル (1) ウソつき問題