CAPG
For any program M in a generic functional language, capg computes a pair of formulae which are the best possible specification of that program in the sense that any other program also meeting that specification is observationally indistinguishable form M. Details of the theory behind capg can be found here.
To download capg click here (Version 0.2, capg is GPL licensed).
$Id: index.html,v 1.6 2006/02/17 15:09:56 martinb Exp $