[said Laurent] > > A quick search on METEOR Ada on http://www.google.com gives: > > http://www.atelierb.societe.com/other_papers/english/using_B/using_B.htm > > http://www.atelierb.societe.com/other_papers/french/utilise_B/utilisation_de_B.htm > > It gives some insight on how the thing was formally validated. There > is the email of an RATP guy in the French version. > > --LG > Yes, this is an interesting article and does mention Ada as the code- level language generated by B. Here's a pointer to a nice article (in English) on "Atelier B" http://www.atelierb.societe.com//PAGE_B/uk/atb-01.htm It is mentioned here that code generators are available for Ada and C. Mike Feldman