Post Analysis Treatments¶
Postanalysis treatments are flagactivated Kind 2 features that are not directly related to verification. The current postanalysis treatments available are
certification,
compilation to Rust,
test generation,
contract generation,
assumption generation,
invariant printing, and
inductive validity core generation
All of them are deactivated by default. Postanalysis treatments run on the last analysis of a system. It is defined as the last analysis performed by Kind 2 on a given system. With the default settings, Kind 2 performs a single, monolithic analysis of the top node. In this case, the last analysis is this unique analysis.
This behavior is changed by the compositional
flag. For example, say Kind 2
is asked to analyze node top
calling two subnodes sub_1
and sub_2
, in
compositional mode. Say also sub_1
and sub_2
have contracts, and that
refinement is possible.
In this situation, Kind 2 will analyze top
by abstracting its two subnodes.
Assume for now that this analysis concludes the system is safe. Kind 2 has
nothing left to do on top
, so this compositional analysis is the last
analysis of top
, Kind 2 will run the postanalysis treatments.
Assume now that this purely compositional analysis discovers a counterexample.
Since refinement is possible, Kind 2 will refine sub_1
(and/or sub_2
) and
start a new analysis. Hence, the first, purely compositional analysis is not
the last analysis of top
.
The analysis where sub_1
and sub_2
are refined is the last analysis of
top
regardless of its outcome (assuming no other refinement is possible).
Long story short, the last analysis of a system is either the first analysis allowing to prove the system safe, or the analysis where all refineable systems have been refined.
The modular
flag forces Kind 2 to apply whatever analysis / treatment the
rest of the flags specify to all the nodes of the system, bottomup.
Postanalysis treatments respect this behavior and will run on the last
analysis of each node.
Prerequisites¶
Some treatments can fail (which results in a warning) because some conditions were not met by the system and/or the last analysis. The prerequisites for each treatment are:
Treatment 
Conditions 
Notes 
certification 
last analysis proved the system safe 
will fail if node is partially defined 
compilation to Rust 

test generation 
system has a contract with more than one mode and the last analysis proved the system safe 

contract generation 
experimental 

assumption generation 
last analysis falsified some property 
generates nontemporal constraints 
invariant printing 

inductive validity core generation 
last analysis proved the system safe 