What is the difference between implicit and explicit in VDM-SL

Question

So as the title explains, what's the difference between the implicit and explicit? Is implicit the function and explicit the operation? or is implicit the overture code and the explicit the VDM-SL specifications itself? I'm kind of confused

Answer 1

Implicit definition is where the function or operation is defined only by means of a (pre- and) post-condition, i.e. Boolean expressions. It does not say how the result in the post-condition is reached (though it implies it by giving the salient properties of the result). Such functions and operations cannot be routinely executed by the interpreter, but are perfectly valid in specifying the contract (assumptions and guarantees).

An explicit function or operation has a body that gives an imperative definition of how to compute the result, and therefore can be executed by the interpreter.