[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.
More information about the Why3-club