From news:comp.object :

The only formal specification I've ever seen which a program could be proven against was an algebraic (sp?) one. Even for simple examples, they tend to become quite complex to read  --IljaPreuss

''It is possible, with practice, to write specifications in a "contract" style that can be converted to formal notation as needed.'' --Myles 

I do it the other way round.

Write the formal specification first, then simply convert the spec into a set of DesignByContract artifacts. Then I use the same spec to quickly derive the set of tests required for the s/w (this process is known as specification-directed testing) .

--StevenPerryman