[Termtools] SRS-standard-certifying

[Frederic Blanqui]

Johannes Waldmann a écrit :

> I see. - This is exactly the point of
> http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=45
> and this incident now underlines its urgency.

Dear all,

for CoLoR and Rainbow, since its source code is publicly and freely 
available under CVS, not only the competition committee but -anyone- can 
try to check the correctness of Rainbow and CoLoR encoding of TPDB 
problems in Coq. See in particular the files pb_of_tpdb.ml, coq_of_pb.ml 
and the part of coq_of_prf.ml starting the proof of termination.

For getting more confidence, we could even go further (and this would 
also save time when running the competition) by generating -before the 
start of the competition- the Coq files encoding the TPDB problems: 
(f_rainbow.xml, f_color.v, f_color.vo, f_cime.v, f_cime.vo for all f). 
Then, during the competition, the Coq files generated by Rainbow could 
simply import the file f_color.

We can also do the following additional syntactic checks on f_color_prf.v:

- The file contains the string "Lemma termin : WF rel." not in a comment
("rel" is the relation defined in f_color.v the termination of which has 
to be proved).

- The file only imports files of the CoLoR library.

- The file does not contain the strings "Axiom", "Variable", 
"Parameter", "Abort", "Admitted".