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
- Top-level declarations
- 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
- Semantics