Paul February 2016

From implicit to explicit function definitions

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.

Answers


Nick Battle February 2016

There is a formal process for the refinement of specifications, though it is quite laborious, especially since there isn't currently tool support for it.

If you preserve the implicit function type signatures and pre/postconditions, then the explicit versions are "certain" to be a refinement, assuming the implementation is correct for all inputs (which is where combinatorial testing can help). Note that you can also give an implementation (body) to a function written in an "implicit" style, which may simplify things:

f(x:nat) r:nat
== x + 1        -- This line added to the implicit spec!
pre x > 10
post r < 100

Post Status

Asked in February 2016
Viewed 2,317 times
Voted 13
Answered 1 times

Search




Leave an answer