Ada: Lot of specification is exported in Ada. We use ghost code to store all states, we generate the transition pridicate but also the invariant. But two problems, occured. The first one is a visibility problem for the record which is private but must be public for ghost variable which have to be public for specifaction. The second problem is that the approache requires existential quantification for inputs and locals. It works for integers and boolean but not for floats. Some complex solution could be found like writing an iterator for floats, expanding all local variable and store all the required inputs in ghost variable.
Ada: Lot of specification is exported in Ada. We use ghost code to store all states,
we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second
problem is that the approache requires existential quantification for inputs and
locals. It works for integers and boolean but not for floats. Some complex
solution could be found like writing an iterator for floats, expanding all
local variable and store all the required inputs in ghost variable.