This chapter introduces two abductive proof procedures for reasoning upon SCIFF (and therefore also CLIMB) specifications:
proof procedure checks whether an execution trace
with a SCIFF specification, providing a concrete operational framework for:
generating positive and negative expectations starting from a trace and a specification;
checking whether the generated expectations are fulfilled by the actual occurring events (hypotheses confirmation step).
is able reason upon a complete execution trace, or upon a growing trace, by dynamically acquiring and processing occurring events as they happen.