examples_in_progress/why3_logic/ident.mlw

   1
   2 (* Very, very abstract views of strings & Why3 locations:
   3    they are. *)
   4 module String
   5   type string
   6 end
   7
   8 module Loc
   9   type position
  10 end
  11
  12 module Label
  13
  14   use String
  15   use Loc
  16
  17   type label model { lab_string : string }
  18
  19   val lab_equal (l1 l2:label) : bool
  20     ensures { result -> l1 = l2 }
  21     ensures { l1.lab_string = l2.lab_string -> result }
  22
  23   val create_label (s:string) : label
  24     ensures { result.lab_string = s }
  25
  26   val lab_string (l:label) : string
  27     ensures { result = l.lab_string }
  28
  29   clone extmap.FMap as Mlab with
  30     type key = label,
  31     type key_l = string,
  32     function k_m = lab_string
  33
  34 end
  35
  36 module Ident
  37
  38   use int.Int
  39   use String
  40   use Loc
  41   use Label
  42   use option.Option
  43   use list.List
  44   use support.HO
  45
  46   (* Abstract name type. *)
  47   type ident_name
  48
  49   (* Not present in Why3: ghost information allowing to know the
  50      identifier class.
  51      Justification: Why3 library make use of the fact that the same identifier
  52      may be used for only one class of variable: variable symbol,
  53      type symbol, function/predicate symbol, proposition symbol, and
  54      maybe others. This fact is used to build maps that are the reunion of
  55      disjoint maps over those categories. *)
  56   type id_class model { id_class_name : ident_name }
  57   (* Type of set of all classes build yet, and of snapshots
  58      of such classes. Correctness of such specification can be
  59      justified via the use of history invariants (this trick is a mere coding
  60      of it)
  61      Important note about this trick: any mean of countourning the fact
  62      that program values of type id_class are build using this interface
  63      would break its safety. In practice, this impose limitation about
  64      calls to logic function in (ghost) code, (axiomatized default/choice break
  65      this property when applied to non-pure logic type such as id_class).
  66      In this setup, the safe logic functions calls in (ghost) code are:
  67      - any call that instantiate polymorphic variables using
  68        pure logic types only (does not interfere with the program world).
  69      - any call to a logic function defined on top of safe logic functions
  70        (can be lifted to the program world).
  71      - projections & constructors (present in the program world).
  72    *)
  73   type id_class_set model { mutable id_classes : id_class -> bool }
  74   type id_class_snapshot model { id_classes_s : id_class -> bool }
  75   val ghost idcls : id_class_set
  76   val ghost id_class_snapshot () : id_class_snapshot
  77     ensures { result.id_classes_s = idcls.id_classes }
  78   val ghost id_classes_growth (id0:id_class_snapshot) : unit
  79     ensures { subset id0.id_classes_s idcls.id_classes }
  80   val ghost id_class_inv (idc:id_class) : unit
  81     ensures { idcls.id_classes idc }
  82   val ghost fresh_id_class () : id_class
  83     writes { idcls }
  84     ensures { not (old idcls).id_classes result }
  85     ensures { subset (old idcls).id_classes idcls.id_classes }
  86     ensures { idcls.id_classes result }
  87
  88   (* Projection. *)
  89   function idn_string ident_name : string
  90   type ident model {
  91     id_name : ident_name;
  92     id_label : string -> bool;
  93     id_loc : option position;
  94     (* Not present in Why3 (because ghost): classes to which the identifier
  95        belong, ordered. This allow to build hierarchies of disjoint name
  96        generators on top of identifiers, while being able to easily recover the
  97        disjointness property. *)
  98     id_class : list id_class;
  99   }
 100
 101   function id_string (i:ident) : string = i.id_name.idn_string
 102
 103   val id_string (i:ident) : string
 104     ensures { result = i.id_string }
 105
 106   val id_label (i:ident) : Mlab.s
 107     ensures { result.Mlab.domain = i.id_label }
 108
 109   val id_loc (i:ident) : option position
 110     ensures { result = i.id_loc }
 111
 112   type preid = {
 113     pre_name : string;
 114     pre_label : Mlab.s;
 115     pre_loc : option position;
 116   }
 117
 118   (* TODO (long term): add a mechanism to get back identifier
 119      fields (mainly labels) from their names. *)
 120
 121   (* Similar mechanism for identifier generation. *)
 122   type id_set model { mutable ids : ident_name -> bool }
 123   type id_set_snapshot model { ids_s : ident_name -> bool }
 124   val ghost ids : id_set
 125   val ghost id_set_snapshot () : id_set_snapshot
 126     ensures { result.ids_s = ids.ids }
 127   val ghost id_set_growth (id0:id_set_snapshot) : unit
 128     ensures { subset id0.ids_s ids.ids }
 129   val ghost id_inv (i:ident) : unit
 130     ensures { ids.ids i.id_name }
 131
 132   val id_equal (i1 i2:ident) : bool
 133     ensures { result -> i1 = i2 }
 134     ensures { i1.id_name = i2.id_name -> result }
 135
 136   val id_register (ghost idc:list id_class) (p:preid) : ident
 137     writes { ids }
 138     ensures { result.id_string = p.pre_name }
 139     ensures { result.id_label = p.pre_label.Mlab.domain }
 140     ensures { result.id_loc = p.pre_loc }
 141     ensures { result.id_class = idc }
 142     ensures { not (old ids).ids result.id_name }
 143     ensures { subset (old ids).ids ids.ids }
 144     ensures { ids.ids result.id_name }
 145
 146   clone extmap.FMap as Mid with
 147     type key = ident,
 148     type key_l = ident_name,
 149     function k_m = id_name
 150
 151 end
 152