True, and there was a question on this topic during the Frama-C and Spark day this year in may in Paris, about similar tools and environments in java. People i

True, and there was a question on this topic during the Frama-C and Spark day this year in may in Paris, about similar tools and environments in java. People in the room cited JML and it being the inspiration for ACSL but the conclusion seemed to be that the proof technology wasn't so advanced and supported ? I'm very interested if you have more info on this, I'd be happy to be mistaken. If you look around there's also EVE (for Eiffel) that B. Meyer mentionned some time ago on his blog. They didn't have to add a specification language or to supplement their original language, it was built in Eiffel from the start :-D. One funny thing about specification languages is that they 'need' to be expressive to be useful. The Ada 2012 specs added lots of sugar to help writing contracts : quantifiers on collections/arrays (for some, for one), if- and case- expressions (pattern matching isn't far) and expression functions... and in Spark 2014 contract-cases. I expect some more in Ada2020. Since contracts must be executable you get all the sugar for your regular Ada too.