Revision 4174a469
Added by Guillaume Davy over 8 years ago
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.coq | ||
|---|---|---|
| 1 |
Goal typed_AltitudeControl_step_post. |
|
| 2 |
Proof. |
|
| 3 |
intros. |
|
| 4 |
eapply Q_inv_inv_AltitudeControl. |
|
| 5 |
Focus 4. |
|
| 6 |
eassumption. |
|
| 7 |
eassumption. |
|
| 8 |
eassumption. |
|
| 9 |
eassumption. |
|
| 10 |
Qed. |
|
| 1 |
(* Generated by Frama-C WP *) |
|
| 11 | 2 |
|
| 12 |
Goal typed_ref_AltitudeControl_step_post.
|
|
| 3 |
Goal typed_AltitudeControl_step_post. |
|
| 13 | 4 |
Proof. |
| 14 | 5 |
intros. |
| 15 | 6 |
eapply Q_inv_inv_AltitudeControl. |
| ... | ... | |
| 206 | 197 |
eassumption. |
| 207 | 198 |
Qed. |
| 208 | 199 |
|
| 200 |
Goal typed_ref_AltitudeControl_step_post. |
|
| 201 |
Proof. |
|
| 202 |
intros. |
|
| 203 |
eapply Q_inv_inv_AltitudeControl. |
|
| 204 |
Focus 4. |
|
| 205 |
eassumption. |
|
| 206 |
eassumption. |
|
| 207 |
eassumption. |
|
| 208 |
eassumption. |
|
| 209 |
Qed. |
|
| 210 |
|
|
| 211 |
Goal typed_ref_AltitudeControl_step_stmt_post_20. |
|
| 212 |
Hint AltitudeControl_step,default,property. |
|
| 213 |
Proof. |
|
| 214 |
Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;try why3 "CVC4" timelimit 10. |
|
| 215 |
why3 "alt-ergo" timelimit 20. |
|
| 216 |
Qed. |
|
| 217 |
|
|
| 218 |
Goal typed_ref_lemma_missing. |
|
| 219 |
Hint missing,property. |
|
| 220 |
Proof. |
|
| 221 |
admit. |
|
| 222 |
Qed. |
|
| 223 |
|
|
| 224 |
|
|
Also available in: Unified diff
Correct some problem related to new bool encoding