-
Notifications
You must be signed in to change notification settings - Fork 8
BicoExplanation
For each classfile, Bico generates a type, signature, and implementation formalized in Coq. This generation is modular. Bico also generates summary files to simplify the use of the definitions.
The main limitation of Bico is due to the size of the Java system library. The classes contained in this library are usually not generated, because the resolving of the dependencies would make Bico generate the Coq formalisation for all the system libraries (more than 200 classes). This is not a problem by itself, but loading the generated files into Coq uses a large amount of time and memory. Therefore, Bico is most useful when applied on user-written class files, where this problem tends not to arise.
Version: 1 Time: Thu Mar 27 12:05:23 2008 Author: dcochran (dcochran) IP: 193.1.132.32