[Why3-club] Module names in files for external provers

Guillaume Melquiond guillaume.melquiond at inria.fr
Thu Mar 6 10:43:01 CET 2014


On 05/03/2014 10:59, Stefan Berghofer wrote:
> Dear Why3-Club,
>
> I am currently using the Isabelle driver for Why3 in connection with the
> tools for
> SPARK 2014, which generate Why3 files containing a large number of
> modules. Unfortunately,
> when generating files for external provers such as Isabelle, the
> information which identifier
> belonged to which module is completely lost. To illustrate the problem,
> I have attached a
> simple example Why3 file containing two modules Foo and Bar, each of
> which contains a type
> t, functions f and g, as well as an axiom ax. The types and functions
> from Foo and Bar are
> then used in the definition of a function bla contained in another
> module Baz. When generating
> verification conditions for bla, the identifiers Foo.t, Foo.f, Foo.g,
> Bar.t, Bar.f and Bar.g are
> turned into t, f, g, t1, f1 and g1 by Why3's name mangling mechanism.
> This is not only unreadable
> but also not very robust, in particular when more modules containing
> similar identifiers are
> added to the Why3 file. To make the generated names more predictable, I
> was wondering whether it
> is possible to extend the driver to also output the module / theory name
> together with an
> identifier. Is there some function in the Why3 API that maps an
> identifier to the name of
> the module / theory in which it was introduced?

(Disclaimer: I am no expert on that part of the code, so take my answer 
with a grain of salt.)

Yes and no. I don't think there is a such function already. But the code 
at the start of printers supporting realizations (including Isabelle) 
already does it, though only for realized theories. By lifting this 
restriction, it should be possible to achieve what you want.

Best regards,

Guillaume



More information about the Why3-club mailing list