Semantics

B3 checks partial correctness. That is, B3 does not enforce termination.