[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] generation of Ada text in PVS



Hi ,

As a new PVS'user, i wonder if it is possible to get a generation Ada 
Text, considering it was previously a feature in EHDM ?

I work on the possibility to specify a clock synchronisation algorithm 
(and on the possible proof), and i would be interested to implement it 
in our PolyORB framework, wich is written in Ada

Thank you by advance,

Best regards,

Isabelle