PlusCal

PlusCal is a simple idealized Imperative Programming Language used in TLA Plus.