The BLESS Book contains:

  • a language reference manual with formal grammar and semantics,
  • a guide to the BLESS IDE within Eclipse,
  • usage of the BLESS Proof Assistant and,
  • and soundness proof for a growing list of proof rules.
BLESS_BookDownload

Sometimes, a quick look at BNF grammar helps figure out how to express what you want. Six syntax cards are provided: the combined BLESS grammar, and the grammars for each of the annex languages: Action, Axiom, State Machine, Type, and Unit.

BLESS Syntax Cards v3Download