🚀 go-pugleaf

I've seen a few references here and there to using formal methods to
specify an already implemented system; the claim is that this exercise
was useful in identifying previously latent errors/ambiguities, and that
the end product was a formal specification that corresponded pretty well
with the implementations.  I'm very interested in this approach, which
seemingly is in the intersection of formal methods, reverse
engineering/design recovery, and (corrective/perfective) maintenance.

Any references, texts, anecdotes, etc. on this topic will be
appreciated. 

If there's enough interest I'll post a summary to the net.

Thanks a lot,
Chuck
--

+------------------------------------------------------------------------+
| Chuck Howell, M/S Z645     INTERNET: howell@community-chest.mitre.org  |
| The MITRE Corporation           OR   howell@mwunix.mitre.org           |
| 7525 Colshire Drive           VOICE: (703) 883-6080                    |
| McLean VA 22102-3481            FAX: (703) 883-5519                    |
+------------------------------------------------------------------------+