-tag mathmodel:t:"Mathematical Model (abstract fields):"
-tag mathdef:t:"Mathematical Definition (derived abstract fields):"
-tag constraint:t:"Constraint (abstract invariant):"
-tag initially:t:"Initial State (ensured by constructor):"
-tag convention:t:"Convention (concrete representation invariant):"
-tag correspondence:t:"Correspondence (abstraction relation):"
-tag param
-tag requires:cm:"Requires (precondition):"
-tag alters:m:"Alters (modification frame):"
-tag ensures:cm:"Ensures (postcondition):"
-tag return -tag throws -tag author -tag version -tag see -tag since