Developer Guide
From the previous sections, you know that JPF is a collection of interchangeable components. In this guide:
Core Mechanisms
- ChoiceGenerators – Non-deterministic choice handling
- Partial Order Reduction – State-space optimization
- Slot and Field Attributes – Custom data storage
Extension Mechanisms
- Listeners – Event-driven JPF extensions
- Search Strategies – Custom exploration algorithms
- Model Java Interface (MJI) – Native method modeling
- Bytecode Factories – Custom instruction implementations
Utilities
- Logging System – JPF’s logging infrastructure
- Reporting System – Output and result reporting
- Running JPF from Application – Embedding JPF
Development Process
- Coding Conventions – JPF coding standards
- Creating Projects – New JPF project setup
- Modules – JPF module architecture