Rodin Handbook
This work is sponsored by the Deploy Project
This work is sponsored by the ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
Rodin User’s Handbook v.2.8 |  |
 |
 |
3.2.7 Generated proof obligations
Table 3.1 shows a brief overview about the different proof obligations that are generated. The user can use this table to identify a specific proof obligation. For further information, a reference to the relevant reference section is provided.
generated in contexts |
||
well-definedness of an axiom |
label/WD |
|
axiom as theorem |
label/THM |
|
generated for machine consistency |
||
well-definedness of an invariant |
label/WD |
|
invariant as theorem |
label/THM |
|
well-definedness of a guard |
event/guardlabel/WD |
|
guard as theorem |
event/guardlabel/THM |
|
well-definedness of an action |
event/actionlabel/WD |
|
feasibility of a non-det. action |
event/actionlabel/FIS |
|
invariant preservation |
event/invariantlabel/INV |
|
generated for refinements |
||
guard strengthening |
event/abstract_grd_label/GRD |
|
action simulation |
event/abstract_act_label/SIM |
|
equality of a preserved variable |
event/variable/EQL |
|
guard strengthening (merge) |
event/MRG |
|
well definedness of a witness |
event/identifier/WWD |
|
feasibility of a witness |
event/identifier/WFIS |
|
generated for termination proofs |
||
well definedness of a variant |
VWD |
|
finiteness for a set variant |
FIN |
|
natural number for a numeric variant |
event/NAT |
|
decreasing of variant |
event/VAR |
|
|
|
|
|
|
|