I have been creating specifications using implicit function definitions in VDM-SL and it has worked out very well. I now want to prototype the specification using explicit function definitions (no operations at this stage).
One way I can see of doing it is to create a new module that mimics the functions defined in the implicit specification, but give them explicit definitions.
I'm sure this could be done but I doubt it is ideal. There would be no link between the implicit and the explicit specification, though one is a refinement of the other.
Is there a recommended way of transitioning from implicit to explicit function definitions. Longer term I do want to investigate doing this formally, but in the first instance I simply want to implement the implicit function specifications to demonstrate the specification in action.