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

Stefan Berghofer berghofe at in.tum.de
Wed Mar 5 10:59:57 CET 2014


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?

Greetings,
Stefan
-------------- next part --------------
module Foo
  use import int.Int

  type t
  function f int : t
  function g t : int

  axiom ax: forall x : int. g (f (x)) = x
end

module Bar
  use import int.Int

  type t
  function f int : t
  function g t : int

  axiom ax: forall x : int. g (f (x)) = x
end

module Baz
  use Foo
  use Bar

  let bla (n : int)
    ensures { result = n } =
    Bar.g (Bar.f (Foo.g (Foo.f n)))
end


More information about the Why3-club mailing list