Quint is a programming language created in 2021.
#970on PLDB | 3Years Old |
git clone https://github.com/informalsystems/quint
A modern and executable specification language.
/// A state variable to store the balance of each account
var balances: str -> int
pure val ADDRESSES = Set("alice", "bob", "charlie")
action withdraw(account, amount) = {
// Decrement balance of account by amount
// Whoops, we forgot to check for enough balance
balances' = balances.setBy(account, curr => curr - amount)
}
// ...
/// Invariant: Account balances should never be negative
val no_negatives = ADDRESSES.forall(addr =>
balances.get(addr) >= 0
)