Home

Forge is a lightweight modeling language, similar to Alloy, that has been designed for teaching modeling and lightweight formal methods. It comprises three sublanguages or modes:

• Froglet (#lang forge/bsl), a core language for modeling using object-oriented intuitions;
• Forge (#lang forge), an extension of Frglet to include relations and relational operators;
• Temporal Forge, an extension of Forge to include linear-temporal operators (akin to Alloy 6 or Electrum).

Students progress through this language hierarchy as new concepts are introduced in class; this lets the course avoid a steep language-learning curve andcover important practical material earlier than would otherwise be possible.

Table of Contents

• Installing Forge
• Types and Fields
• Constraints
  • Logical Operators
  • Relational Operators
  • Defining Predicates and Functions
  • Quantifiers
  • Temporal Operators (Electrum Mode)
• Built-ins: Constants, Relations, and Helpers
  • Constants
  • Sequences and Reachability
  • Integers
• Running
  • Running Your Model
  • Visualizing Instances (including custom scripts)
  • Testing Your Model (Tests and Examples)
  • Forge Options
  • Details on Bounds (and Instance Bounds)