[Why3-club] constraint-pvs generated file

Dragan dragan.stosic at gmail.com
Mon Nov 18 21:45:44 CET 2013


Hi all,
There is a constraint I found working with pvs files generated by
frama-c/jessie/why3.
Here is simple example and suggestion how to fix  potential issue.
Suppose we have VC foo, splitted into two goals: foo_1 and foo_2.
Adding/editing PVS , the system will generate two separate files: foo_1.pvs
and foo_2.pvs.
Unfortunately, both files contains  the same (unique) name of the theories
and theorems.
We can conclude:  it is not possible to re-use theories by importing in
other theories.
This problem can be fixed using the following strategy:
1 ) foo_1.pvs
         foo_1:THEORY
          foo_1:THEOREM forall ...
         END foo_1
2) foo_2.pvs
         foo_2:THEORY
         foo_2:THEOREM forall ...
         END foo_2
3) foo.pvs
    foo:THEORY
        IMPORTING foo_1, foo_2
    END foo
Therefore we can  separate theories per files, as it is shown above, and we
would be able to import any of
those theories , avoiding name constraint issue (duplication) and potential
type checking error.
I believe that it is not big issue to fix in the code and I am fairly sure
that the whole frama-c/why3/PVS community will be really grateful.
Best Regards

-- 
Dragan Stosic
Senior developer at IBM
phone: 085-773-1050
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
Mulhuddart
Dublin 15
Ireland
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131118/47c02391/attachment.html>


More information about the Why3-club mailing list