When there is no explicit contract for a method, KeY adds a default contract. This option determines whether to use a sound or unsound default. Using the unsound default may be useful during development.
Unspecified methods get the following default contract:
public behavior
ensures true;
diverges true;
signals_only Throwable;
assignable \everything;
Unspecified method get the following unsound default contract:
public normal_behavior
ensures true;
assignable \strictly_nothing;