[Why3-club] constraint-pvs generated file
dragan.stosic at gmail.com
Mon Nov 18 21:45:44 CET 2013
There is a constraint I found working with pvs files generated by
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
Unfortunately, both files contains the same (unique) name of the theories
We can conclude: it is not possible to re-use theories by importing in
This problem can be fixed using the following strategy:
1 ) foo_1.pvs
foo_1:THEOREM forall ...
foo_2:THEOREM forall ...
IMPORTING foo_1, foo_2
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.
Senior developer at IBM
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club