Multi-line contract syntax

Single-line assertion syntax

Contracts before declarations

\valid for struct pointer

\valid for out pointer

\separated usage

assigns clause on rb_write

assigns clause on rb_read

assigns \nothing / minimal on rb_reset

Return value postcondition — success path

Return value postcondition — failure path

Explanatory comments on non-obvious specs

integer type in quantifiers

loop invariant present — count_in_range

loop assigns present — count_in_range

loop variant present — count_in_range

loop invariant present — replace_char

loop assigns present — replace_char

loop variant present — replace_char

Loop annotations before loop header

integer type in loop invariant quantifiers

Function assigns clause — count_in_range

Function assigns clause — replace_char

\valid_read for const pointer

Invariant bounds loop counter

Result postcondition

behavior blocks in safe_divide

complete behaviors — safe_divide

disjoint behaviors — safe_divide

behavior blocks in abs_value

complete behaviors — abs_value

disjoint behaviors — abs_value

Reusable predicate or logic definition

decreases clause on gcd

assigns \nothing on pure functions

\result postcondition — safe_divide zero case

\result postcondition — abs_value

gcd postcondition — divisibility

assumes clause in behaviors