Home¶
This documentation is for Forge version 4.
This is the documentation page for Forge version 4. The documentation for Forge version 5 is available for that version.
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/froglet), a language for modeling using only functions and partial functions; - Relational Forge (
#lang forge), an extension of Froglet to include relations and relational operators; - Temporal Forge (
#lang forge/temporal), an extension of Forge to include linear-temporal operators (akin to Alloy 6 or Electrum).
Students can progress through this language hierarchy as new concepts are introduced in class; this lets the course avoid a steep language-learning curve and cover important practical material earlier than would otherwise be possible.
If there are three languages, are there three versions of the documentation?
No! In principle, we might ideally have three separate versions, but we are focusing (for now) on producing better documentation overall rather than taking on the subtle cross-language page-linking challenge.
We will nevertheless try to maintain a reasonable separation.
Textbook¶
Forge also has a draft textbook, which is in a different document in order to make searching easier.
Using this Documentation¶
Navigation, Theme, and Search
- Navigation: Use the sidebar on the left to browse sections. Click section headers to expand subsections.
- Search: Use the search bar at the top, or press ++s++ to open search.
- Theme: Click the theme toggle icon (sun/moon) in the header to switch between light and dark modes.
- Version: If available, use the version selector in the header to switch between documentation versions.