D. Peters, und D. Parnas. IEEE Transactions on Software Engineering, 24 (3):
161--173(1998)ST: Spezifikation einer SW-Einheit (im Paper Methoden) wird formal beschrieben. Tool leitet automatisch Orakel ab.
Grenzen werden bei dynamische Datenstrukturen erreicht da sie schwer beschreibbar sind.
Die formale Spezifikation erscheint in den Beispielen sehr aufwendig..
A. van Lamsweerde. ICSE '00: Proceedings of the Conference on The Future of Software Engineering, Seite 147--159. New York, NY, USA, ACM, (2000)MR: Wertvoll wegen dem Überblick über formale Spezifikations- und somit Modell-Paradigmen..