How to Read this book
Preamble: Beyond Testing
What good is this book?
Logic for Systems
From Tests to Properties
Modeling Static Scenarios
Tic-Tac-Toe
Binary Search Trees
Ripple-Carry Adder
Q&A: Static Modeling
Discrete Event Systems
Transitions, Traces, and Verification
Counterexamples to Induction
BSTs: Recursive Descent
Validating Models (in progress)
Q&A: Event Systems (in progress)
Modeling Relationships
Relational Forge, Modeling Logic
Transitive Closure
Modeling Mutual Exclusion
Going Beyond Assertions
How does Forge Work?
Q&A: Relations
Temporal Specification
Liveness and Lassos
Temporal Forge
Linear Temporal Logic
Obligations and the Past
Mutual Exclusion, Revisited
Additional Examples, Case Studies, and Further Reading
Modeling Raft in Anger (in progress)
Forge: Comparing Prim's and Dijkstra's Algorithms (in progress)
Forge+Industry: Policy and Network Analysis (in progress; DEMO: ABAC, Margrave, Zelkova)
Forge+Industry: Crypto Protocol Analysis (in progress; DEMO: crypto lang, CPSA or other)
Program Synthesis (in progress; DEMO: SSA synth, Sygus)
Further Reading (in progress)
Construction Storage
DPLL (to edit)
Propositional resolution (to edit)
Forge Documentation
Forge Version
Installation
Overview
❱
1. Addendum for Alloy Users
Sigs
❱
Constraints
❱
Comments
Running
Sterling Visualizer
Bounds
❱
1. Concrete Instance Bounds
Options
Testing
Integers
Constants and Keywords
Helpers: Sequences and Reachability
Temporal Forge Overview and Operators
Custom Visualization Basics
❱
1. D3FX Helpers (April 2023)
2. Working with SVG and Imports
Attribute-Based Access Control
What should I do if...

Logic for Systems: Lightweight Formal Methods for Everybody

Formulas

Formulas are a type of Forge syntax. Given an instance, every formula evaluates to a boolean value. If the formula is true of an instance, we say that the instance satisfies the formula.