Added by Guillaume DAVY almost 3 years ago
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.
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
let instantiated_types = snd (List.split substitution) in
fprintf fmt "%t%t%a"
fprintf fmt "%t_inst%t%a"
(Utils.pp_final_char_if_non_empty "_" instantiated_types)
(Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
Also available in: Unified diff