[Why3-club] Krakatoa - specifying third party libraries

Claude Marche Claude.Marche at inria.fr
Thu Feb 16 21:53:56 CET 2012


I've just answered the question on the Why-discuss list, which is a 
better place for questions about Krakatoa.

- Claude

On 02/16/2012 09:34 PM, João Paulo Carvalho wrote:
> Hi,
>
>
> 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.
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club




More information about the Why3-club mailing list