[Why3-club] Krakatoa - specifying third party libraries

João Paulo Carvalho joao_paulo_c at yahoo.com
Thu Feb 16 21:34:26 CET 2012


Does Krakatoa have any feature to specify a class library or framework when one doesn't have access to the source code?

What I'm interested is to formally specify the intention behavior (as in the manual) of the library, assume it is true, and formally verify the client code of this library (which we have the source code) assuming that the library does what it says (manual) it does.

João Paulo.

More information about the Why3-club mailing list