This is B3

B3 is an intermediate verification language (IVL). It is used to prescribe proof obligations, primarily those of interest in an automated deductive verifier for a source programming language.

B3 is an open-source project on github.

Contents:

• Motivation
• Examples
• General syntax
  • About the grammar notation
  • Comments
  • Self-terminating statements and expressions
  • Order of declarations
• Top-level declarations
  • Types
  • Taggers
  • Functions
  • Axioms
  • Procedures
• Statements
  • Variable declarations
  • Assignment statements
  • Re-init statements
  • Block statements
  • Call statement
  • Check statements
  • Assume statements
  • Reach statements
  • Assert statements
  • Forall statements
  • Choose statements
  • If statements
  • If-case statements
  • Loops
  • Labeled statements
  • Exit statements
  • Return statements
  • Probe statements
• Expressions
  • Literal expressions
  • Identifier expressions
  • Operator expressions
  • Function calls
  • Labeled expressions
  • Let expressions
  • Quantifier expressions
• Convenience features
  • Auto-invariants
• Semantics