[Why3-club] modules and names

Andrei Paskevich andrei at tertium.org
Thu Feb 16 18:06:12 CET 2012

On Thu, 16 Feb 2012 at 16:41:31 (+0100), Johannes Kanig wrote:
> 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?

One possibility would be to give reasonably long names to identifiers
(e.g. "type std_integer") and then "use Standard_integer as SI", so that
the qualified name would be "SI.std_integer".


More information about the Why3-club mailing list