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

254 Views Asked by At

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

1

There are 1 best solutions below

0
On BEST ANSWER

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.