DSL for specifying systems via linear temporal logic. Enables model checking against implementations with Kotest or Scalacheck integration and property verification using Alloy integration.
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:
The use of temporal logic to describe program properties has a long history. Some interesting pointers are:
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:
The use of temporal logic to describe program properties has a long history. Some interesting pointers are:
