В чем разница между неявным и явным в VDM-SL

Итак, как понятно из названия, в чем разница между неявным и явным? Является ли неявная функция и явная операция? или это неявный предварительный код и явные спецификации самой VDM-SL? я немного запутался

1 ответ

Неявное определение – это когда функция или операция определяются только с помощью (предварительного и) постусловия, т.е. логических выражений. В нем не говорится, как достигается результат в постусловии (хотя и подразумевается, давая существенные свойства результата). Такие функции и операции не могут выполняться интерпретатором в обычном порядке, но вполне допустимы при спецификации контракта (допущения и гарантии).

Явная функция или операция имеет тело, которое дает императивное определение того, как вычислить результат, и поэтому может быть выполнена интерпретатором.

Другие вопросы по тегам