SPECIFICATION Spec
CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.