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.
/*!
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.
*/ soundDefaultContracts : { /*!
Unspecified methods get the following default contract:
public behavior
ensures true;
diverges true;
signals_only Throwable;
assignable \everything;
*/ on , /*!
Unspecified method get the following unsound default contract:
public normal_behavior
ensures true;
assignable \strictly_nothing;
*/ off } defined in: soundDefaultContracts.key Line: 2 Offset :4Unspecified 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;