equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 subsubsection "VCG for Total Correctness With Logical Variables" |
2 |
4 |
3 theory VCG_Total_EX2 |
5 theory VCG_Total_EX2 |
4 imports Hoare_Total_EX2 |
6 imports Hoare_Total_EX2 |
5 begin |
7 begin |
6 |
|
7 subsection "Verification Conditions for Total Correctness" |
|
8 |
8 |
9 text \<open> |
9 text \<open> |
10 Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables. |
10 Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables. |
11 As a result the completeness proof runs into a problem. This theory uses a Hoare logic |
11 As a result the completeness proof runs into a problem. This theory uses a Hoare logic |
12 with logical variables and proves soundness and completeness. |
12 with logical variables and proves soundness and completeness. |