Specification-based retrieval provides exact contentoriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any deduction into an offline indexing phase. In this paper, we show how match relations are used to build an appropriate index and how formal concept analysis is used to build a suitable navigation structure. This structure has the single-focus property (i.e., any sensible subset of a library is represented by a single node) and supports attribute-based (via explicit component properties) and object-based (via implicit component similarities) navigation styles. It thus combines the exact semantics of formal methods with the interactive navigation possibilities of informal methods. Experiments show that current theorem provers can solve enough of the emerging proof problems to make browsing feasible. The navigation struco indicates situations where additional abstractions are required to build a ...
B. Fischer