Temporal Logic for JVM
Karat is a DSL to specify systems using linear temporal logic. From a single specification you can pursue two different avenues:
- Check the implementation against the model,
- Using our integration with Kotest if you use Kotlin,
- Or with our integration with Scalacheck if you use Scala;
- Verify properties of the model using our integration with Alloy.
The use of temporal logic to describe program properties has a long history. Some interesting pointers are:
- Quickstrom's Specification Language. Quickstrom is a tool for testing how a web application behaves when some events like clicking occur. It uses temporal logic to express the desired outcome.
- Formal Software Design with Alloy 6. Alloy is a tool for formal modeling and exploration of systems. In Alloy you use temporal logic to both describe the system and specify properties which should be verified.
