« Previous | Next » 

Revision 173a2a8f

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.

View differences:

42 42
43 43
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
44 44

let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr

45 47

46 48

47 49

153 155
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
154 156
            polymorphic_types substituion);
155 157
  let instantiated_types = snd (List.split substitution) in
  fprintf fmt "%t%t%a"
  fprintf fmt "%t_inst%t%a"
157 159
    (pp_package_name machine)
158 160
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
159 161
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types

Also available in: Unified diff