Difference between revisions of "Cascade User Manual"
From CVC4
(→Control File) |
(→Control File) |
||
Line 4: | Line 4: | ||
= Control File = | = Control File = | ||
+ | |||
+ | Instead of inserting annotations in the source code, Cascade keeps them in a control file in order to leaves the source code clean. The control file is in the simple XML format, which serves as the guidance of verification. In this section, we will introduce the elements included control files by showing how to verify some sample codes in Cascade. | ||
== Basic Structure == | == Basic Structure == |
Revision as of 10:16, 12 December 2012
Getting Cascade
Using Cascade
Control File
Instead of inserting annotations in the source code, Cascade keeps them in a control file in order to leaves the source code clean. The control file is in the simple XML format, which serves as the guidance of verification. In this section, we will introduce the elements included control files by showing how to verify some sample codes in Cascade.