2. Correctness checking features
Constructs in this section may serve only some of the analyses listed under sub-goal 1; an analysis
that does not use a construct treats it as absent. assume statements are the simplest example:
during execution an assume is a no-op, so assume false; assert false; assert false reports the
two assertions as failing and does nothing with the assume, while deductive verification uses the
assume as a hypothesis and discharges both assertions. This complements goal 7: erasability
protects execution behavior, and ignorability protects each analysis from the constructs it does
not need.