[Why3-club] modules and names

Johannes Kanig kanig at adacore.com
Thu Feb 16 16:41:31 CET 2012

Hello Why3 team,

Following a recent suggestion of yours, we wanted to get rid of "use
import" to only use "use", and use prefixed objects instead.

Today, we do (for example)

  module Standard_integer
    type standard_integer
    (* more declarations here *)

  module Elsewhere
    use import Standard_integer
    (* use the type *)
    ... standard_integer ...

With your suggestion (do not use "use import"), we tend to write the

  module Standard_integer
    type t
    (* more declarations here *)

  module Elsewhere
    use Standard_integer
    (* use the type *)
    ... Standard_integer.t ...

The problem with this approach is that in generated VCs, all types will
be called "t", with numeric suffixes, ie t1, t2, t35, etc. It becomes
impossible to read the VCs, especially if the same approach is followed
for variable names.

The alternative would be to leave the long name, but then we would need
to refer to it via "Standard_integer.standard_integer", which is much
too long (many names in our system our much longer).

Do you have a suggestion for me, how to deal with this problem? Or maybe
could why3 use the module/theory name to generate a name for the VCs?

Thanks in advance,


Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list