The Coq mailing list

[Velasco Manu <manu.velasco AT caramail.com>]

Hello, I'm a spanish student and my english isn't very well, so I want to excuse at the first about that.

 

I have to make a proove with coq. I have read the tutorial but I still haven't a good idea of the tool and its possibilities.

 

I'm going to describe my subject and I will be very thankfull if somebody can help me.

 

I start with this information:

  - The description of the syntax rules of the language in BNF format.

  - A precondition that must to be checked for do an insertion of one element before a selection of the map inside of an englobant. Where element, selection and englobant are parameters.

 

The map that results after the insertion must to be correct.

 

I know that this information it's not such, but it is an introduction of the problem that I have to solve.

 

Thank you very much. I hope yours responses.

______________________________________________________________
Gagne une PS2 ! Envoie un SMS avec le code PS au 61166
(0,35 Euro Hors coût du SMS)