(* Author: Tobias Nipkow *) subsubsection "VCG for Total Correctness With Logical Variables" theory VCG_Total_EX2 imports Hoare_Total_EX2 begin text ‹ Theory ‹VCG_Total_EX› conatins a VCG built on top of a Hoare logic without logical variables. As a result the completeness proof runs into a problem. This theory uses a Hoare logic with logical variables and proves soundness and completeness. › text‹Annotated commands: commands where loops are annotated with invariants.›